create Index Linked List from a plain List

Question

I'm currently playing with an indexed linked list. The basic data type is given by

data LList (n :: Nat) (a :: Type) where
  Nil  ::LList 0 a
  (:@) ::a -> LList n a -> LList (n + 1) a

I was wondering whether it's possible to define a mapping from [] to LList?

The return type depends on runtime information as the length of the list is, of course, not available at compile time.

fromList :: ? => [a] => LList ? a
fromList = undefined

The full source code of the playground is available here.

Answer 1

Yes, just use an existential. This wraps the length of the list and the list itself into a pair, which does not show its length in the type.

data SomeLList a = forall n. SomeLList (LList n a)

This says that a SomeLList a consists of a term of the form SomeLList @(n :: Nat) (_ :: LList n a). This type is in fact equivalent to [] (except for an extra bottom and no infinities)

fromList :: [a] -> SomeLList a
fromList [] = Nil
fromList (x : xs) | SomeList xs' <- fromList xs = SomeList (x :@ xs)

You get the type out of the pair by matching:

something :: [a] -> ()
something xs
  | SomeList xs' <- fromList xs
  = -- here, xs' :: SomeList n xs, where n :: Nat is a new type (invisibly) extracted from the match
    -- currently, we don't know anything about n except its type, but we could e.g. match on xs', which is a GADT and could tell us about n
    ()