Transform list in type fixed length in haskell-CodePudding

With the answer to this question I was able to define a list in witch the length is part of the type:

{-# LANGUAGE DataKinds, GADTs, KindSignatures #-}

data Nat = Z | S Nat

data ListF (n :: Nat) a where
    Nil :: (ListF 'Z a)
    Cons :: a -> ListF m a -> ListF ('S m) a

I would like be able to convert a normal list in to these kind of list. If a make these:

toListF :: [a] -> ListF n a
toListF [] = Nil
toListF (x:xs) = Cons x (toListF xs)

It does't type-check, because for [a] -> ListF n a to type-check, the function should return any Nat that the caller needs:

ListF.hs:11:14: error:
    • Couldn't match type ‘n’ with ‘'Z’
      ‘n’ is a rigid type variable bound by
        the type signature for:
          toListF :: forall a (n :: Nat). [a] -> ListF n a
        at ListF.hs:10:1-27
      Expected type: ListF n a
        Actual type: ListF 'Z a
    • In the expression: Nil
      In an equation for ‘toListF’: toListF [] = Nil
    • Relevant bindings include
        toListF :: [a] -> ListF n a (bound at ListF.hs:11:1)
   |
11 | toListF [] = Nil
   |              ^^^
Failed, no modules loaded.

The logical type for toListF I think it wold be something like exists n. [a] -> ListF n a or [a] -> (exists n. ListF n a), but of course those are not valid haskell types.

It is possible to do what I am trying to do in haskell? And how?

CodePudding user response：

There are existential types in Haskell.

{-# LANGUAGE DataKinds, GADTs, KindSignatures, RankNTypes #-}

data Nat = Z | S Nat

data ListF (n :: Nat) a where
    Nil :: (ListF 'Z a)
    Cons :: a -> ListF m a -> ListF ('S m) a

data SomeListF a = forall n . AList (ListF n a)

You cam convert from a regular list to SomeListF:

fromList :: [a] -> SomeListF a
fromList [] = AList Nil
fromList (x:xs) = someCons x (fromList xs) where
   someCons x (AList zs) = AList (Cons x zs)

You can also recover ListF from SomeListF, but only in a restricted scope. The n in forall n cannot escape, so you cannot have something like

toListF :: SomeListF a -> ListF n a

but you can have this:

withSomeList :: (forall n . ListF n a -> b) -> SomeListF a -> b
withSomeList f (AList zs) = f zs

Inside the f argument, n is known and you can for example map your list and the length of the result is statically known to be the same as the length of the argument. Here's a silly example:

zipF :: ListF n a -> ListF n b -> ListF n (a, b)
zipF Nil Nil = Nil
zipF (Cons y ys) (Cons z zs) = Cons (y, z) (zipF ys zs)

mapF :: (a->b) -> ListF n a -> ListF n b
mapF _ Nil = Nil
mapF f (Cons z zs) = Cons (f z) (mapF f zs)

zipMapF :: (a->b) -> ListF n a -> ListF n (a, b)
zipMapF f zs = zipF zs (mapF f zs)

zipMapAny :: (a->b) -> ListF n a -> SomeListF (a, b)
zipMapAny f zs = AList (zipMapF f zs)

nums = fromList [1,2,3,4,5]
numsAndSquares = withSomeList (zipMapAny (\x -> x * x)) nums

zipMapAny "knows" that the length of all the lists inside it is the same, but it cannot leak that length to the result. You cannot have for example withSomeList (zipMapF (\x -> x * x)) nums because n would escape.