Reading dependently-sized vectors.

depparse.hs

-- http://www.reddit.com/r/haskell/comments/1z8wsv/prove_your_haskell_for_great_safety_part_i/cfrqwdf
-- http://hackage.haskell.org/package/monomorphic-0.0.3.0/docs/Data-Type-Monomorphic.html

fromList :: [a] -> Monomorphic (Vector a)
fromList [] = Monomorphic Nil
fromList (x : xs) =
  case fromList xs of
    Monomorphic vs -> Monomorphic $ x :- vs

readVector :: Read a => String -> Monomorphic (Vector a)
readVector = fromList . read

-- readVector can return the empty vector (e.g. readVector "[]" == Monomorphic Nil) 
-- so you can't take head of it.
-- One way to ensure the non-empty of the parsed vector is to quantify over n of Vector (S n) 
-- instead of Vector n:
newtype (:.:) f g a = Compose { getComposed :: f (g a) }
fromNonEmpty :: [a] -> Monomorphic (Vector a :.: S)
fromNonEmpty (a : as) =
  case fromList as of
    Monomorphic vs -> Monomorphic $ Compose $ a :- vs

readNonEmptyVector :: Read a => String -> Monomorphic (Vector a :.: S)
readNonEmptyVector = fromNonEmpty . read

main = case readNonEmptyVector "[12]" of
         Monomorphic (Compose vs) -> print (head vs :: Int)
-- One disadvantage of this style is too much Compose things. 
-- Also, you can just define the new existential type for non-empty vectors like 
-- data NonEmpty a = forall n. NonEmpty (Vector a (S n)) and use it.