How to define a family of type dependent function in Haskell

Question

This is a (series of) Haskell question(s). I am fairly new to Haskell.

Suppose we have a 4-tuple (a1,a2,a3,a4). How do we define a function, kth, that gives the k-th element in this tuple? Example,

kth (1,"A",'b',True) 3 = 'b'

If the types of a1, a2, a3, a4 are the same, then it has a fairly simple definition. For example, if they are all integers:

kth :: (Int,Int,Int,Int) -> Int -> Int
kth (a1,a2,a3,a4) 1 = a1
kth (a1,a2,a3,a4) 2 = a2
kth (a1,a2,a3,a4) 3 = a3
kth (a1,a2,a3,a4) 4 = a4

My suspicion of why this is not straightforward is because Haskell must know the type in advance. In the library function fst and snd, Haskell knows that the output type is the type of the first element for the formal, and the output type is the type of the second element for the latter. Hence, there is no ambiguity. In kth, the output type depends on the second input, hence Haskell cannot do type check based on the syntax.

Now, suppose we have a n-th tuple (a1,a2,...,an). Can we define a family of length functions such that

lengthTuple :: a -> Int
lengthTuple (a1,a2,...,an) = n

Answer 1

This kind of problem (dependent type) is still a headache in Haskell. The Tuple from Prelude is not quite suitable for this kind of task (perhaps doable though). But you can use the sized vector with dependent type for this kind of problem.

Example: https://www.schoolofhaskell.com/user/konn/prove-your-haskell-for-great-safety/dependent-types-in-haskell

Answer 2

You can not implement your function if the index must be an Int, but you could if that were a custom "singleton" index type. Essentially, if we want to mimic dependent types, the best option we have is to pass singletons around a lot, to connect type-level values to term-level ones.

Here is one example:

{-# LANGUAGE GADTs, DataKinds, TypeFamilies #-}
{-# OPTIONS -Wall #-}

-- custom index type
data Ix = I1 | I2 | I3 | I4

-- associated singleton type (this could be autogenerated using the singletons library)
data SIx (ix :: Ix) where
  SI1 :: SIx 'I1
  SI2 :: SIx 'I2
  SI3 :: SIx 'I3
  SI4 :: SIx 'I4

-- type level function
type family T (ix :: Ix) a1 a2 a3 a4 
type instance T 'I1 a1 _ _ _ = a1
type instance T 'I2 _ a2 _ _ = a2
type instance T 'I3 _ _ a3 _ = a3
type instance T 'I4 _ _ _ a4 = a4

-- our "dependent" tuple selector
choose :: (a1, a2, a3, a4) -> SIx ix -> T ix a1 a2 a3 a4
choose (x1, _, _, _) SI1 = x1
choose (_, x2, _, _) SI2 = x2
choose (_, _, x3, _) SI3 = x3
choose (_, _, _, x4) SI4 = x4

If wanted, we can "hide" the ix parameter of SIx ix and T ix a1 a2 a3 a4 using an existential wrapper (as a sort of dependent sum type), building a function that given "some index" returns "some component".

This would be much more convenient if we had real dependent types. Still, this is the price we currently pay to have type erasure at runtime. If Haskell one day adds non-erased pi a . ... types to the erased ones forall a . ... we have now, we will have much more control.

Answer 3

The short answer, as suggested in some comments, is that you shouldn't seriously be doing this in Haskell. If you find yourself needing to write functions that can operate on differently sized tuples, you're programming Haskell wrong.

However, the idiomatic method of defining a function like lengthTuple is to use type classes with explicit instances for different tuple sizes. If this is for a library, you pick some upper bound and write instances up to that size. A reasonable choice might be a 15-tuple, since that's also the largest tuple that has a Show instance:

> (1,2,3,4,5,6,7,8,9,10,11,12,13,14,15)
(1,2,3,4,5,6,7,8,9,10,11,12,13,14,15)
> (1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16)
<interactive>:72:1: error:
    • No instance for (Show ...

So, the definition for lengthTuple would look like this:

class Tuple a where lengthTuple :: a -> Int
instance Tuple (a,b) where lengthTuple _ = 2
instance Tuple (a,b,c) where lengthTuple _ = 3
instance Tuple (a,b,c,d) where lengthTuple _ = 4
...up to 15...

Tedious, but pretty standard.

Remarkably, it is possible to write lengthTuple without any boilerplate using Data.Data generics. These generics provide a way to fold over the structure of an algebraic data type in a fairly general way, and you can use a Const functor to ignore the actual content of the data type while counting the number of fields:

import Data.Data
import Data.Functor.Const
lengthTuple :: (Data a) => a -> Int
lengthTuple = getConst . gfoldl (\(Const n) _ -> Const (n+1))
                                (\_ -> Const 0)

This works fine, though there's no straightforward way to restrict it to tuples, and you may find its return value for non-tuples somewhat surprising:

> lengthTuple (1,2,3,4)
4
> lengthTuple ""
0
> lengthTuple "what the heck?"
2

Writing kth is much, much harder. Your intuition is right. Because the type of the expression kth tuple n depends on the value rather than the type of the parameter n, a simple definition isn't possible. The other answers have covered a couple of approaches.