Attempting to collapse functions results in the wrong type

Question

I have the following source code:

{-# LANGUAGE FlexibleContexts, MultiParamTypeClasses, FunctionalDependencies #-} class Digit d data Zero data One data Two data Three data Four data Five data Six instance Digit Zero instance Digit One instance Digit Two instance Digit Three instance Digit Four instance Digit Five instance Digit Six class Sum abc | ab -> c, ac -> b, cb -> a incSize :: (Digit z, Digit x, Sum x One z) => x -> z --written by me incSize _ = undefined intToSize :: (Digit x, Num a, Sum x One x) => a -> x -> t --inferred by GHCI intToSize nv = intToSize (n-1) (incSize v) intToSize' :: (Digit b, Sum b One b) => Int -> t -> b -> b --inferred by GHCI intToSize' nv = foldr (.) id (replicate n incSize) intToSize'' :: (Digit a, Digit b1, Digit b, Digit c, Sum a One b1, Sum b1 One b, Sum b One c) => a -> c --inferred by GHCI intToSize'' = incSize . incSize . incSize 

Essentially, the goal is to take an Int and convert it to one of the data types defined above. The incSize function works correctly; it increases the size by one. The inToSize'' function also works; it will increase the given number by 3. However, both intToSize and intToSize' do not work; GHCI describes their types as described above (and obviously a + 1 = / = a). I’m not sure that manual recording of the composition works correctly, while something else will not work (functions that I have defined as not compiled, but will always give an error when they are used.) The use should look something like this:

 > :t intToSize'' (undefined :: Zero) > intToSize'' (undefined :: Zero) :: Three 

However, the ultimate goal is to write a function that takes a list and gives a data type that encodes the length of the list by type (essentially a vector):

 data Vect sv = Vect v instance forall sv . Show (Vect sv) where --toInt is a function which takes a type number and returns its data level value show (Vect v) = "Vect " ++ (show . toInt) (undefined :: s) ++ show v > let l = [1,2,3,4,5] > vector l > Vect 5 [1,2,3,4,5] 

You may have noticed that the code is missing; it's pretty boring to watch, so I turn it on below.

 instance Sum Zero Zero Zero instance Sum Zero One One instance Sum Zero Two Two instance Sum Zero Three Three instance Sum Zero Four Four instance Sum Zero Five Five instance Sum Zero Six Six instance Sum One Zero One instance Sum One One Two instance Sum One Two Three instance Sum One Three Four instance Sum One Four Five instance Sum One Five Six instance Sum Two Zero Two instance Sum Two One Three instance Sum Two Two Four instance Sum Two Three Five instance Sum Two Four Six instance Sum Three Zero Three instance Sum Three One Four instance Sum Three Two Five instance Sum Three Three Six instance Sum Four Zero Four instance Sum Four One Five instance Sum Four Two Six instance Sum Five Zero Five instance Sum Five One Six instance Sum Six Zero Six 

Answer 1

The problem is that you want to pass a polymorphically typed function to foldr . Note that although foldr itself is of a polymorphic type, it expects its argument to be of a monomorphic type.

For functions that accept polymorphic functions as arguments (and actually use these argument functions are polymorphic), you need a so-called higher rank polymorphism. The good news is that GHC supports higher rated polymorphic types (use the RankNTypes extension); the bad news is that the type of output is unsolvable for them. Therefore, you will need explicit type signatures in your code to convince the validating type that your code is correct. The question then becomes, what will be the type signature that you need for your intToSize' function? And then the worse news comes up: since the type of your function must depend on the integer value you provide, it cannot be directly expressed in Haskell.

---

However, with GADT and family types, you can go a long way towards what you think after:

 {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeFamilies #-} data Zero data Succ n type One = Succ Zero type Two = Succ One type Three = Succ Two data Nat :: * -> * where Zero :: Nat Zero Succ :: Nat n -> Nat (Succ n) zero = Zero one = Succ zero two = Succ one three = Succ two type family Sum mn :: * type instance Sum Zero n = n type instance Sum (Succ m) n = Succ (Sum mn) add :: Nat m -> Nat n -> Nat (Sum mn) add Zero n = n add (Succ m) n = Succ (add mn) incSize :: Nat m -> Nat (Sum One m) incSize = add one -- or just: Succ 

For instance:

 > :t incSize two incSize two :: Nat (Sum One (Succ (Succ Zero))) 

and note that Sum One (Succ (Succ Zero))) same as Three .

---

As for your big goal, by writing “a function that takes a list and gives a data type that encodes the length of the list in its type”: you simply cannot do this. You cannot have a function with a static (i.e. compilation time) depending on a value (list length) that may not be known until runtime.

The closest you can get is to wrap your vector type in an existential wrapper:

 {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeFamilies #-} data Nat = Zero | Succ Nat data Vec :: Nat -> * -> * where Nil :: Vec Zero a Cons :: a -> Vec na -> Vec (Succ n) a data EVec :: * -> * where Exists :: Vec na -> EVec a enil :: EVec a enil = Exists Nil econs :: a -> EVec a -> EVec a econs x (Exists xs) = Exists (Cons x xs) vector :: [a] -> EVec a vector = foldr econs enil 

Now that you have a value of type EVec , you can open it and subject the contained vector to all types of processing with increased type safety, which is enabled by encoding its length in your type.