Haskell: Existential Types and IO

Question

       Cross-posted at Code Review SE

In my attempts to grasp Existential Types in Haskell I decided to implement an integer-based fixed-length vector data type. I'm using ghc 7.8.3.

Specifically I wanted to write a program which asks the user for a possible new value to append to a fixed-length vector and then displays the resulting vector.

First I wrote a first version of the program like this:

{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE Rank2Types                #-}

import System.IO (hFlush, stdout)

data Z
data S n

data Vect n where
    ZV :: Vect Z
    CV :: Int -> Vect n -> Vect (S n)

data AnyVect = forall n. AnyVect (Vect n)

instance Show (Vect n) where
    show ZV = "Nil"
    show (CV x v) = show x ++ " : " ++ show v

vecAppend :: Int -> Vect n -> Vect (S n)
vecAppend x ZV = CV x ZV
vecAppend x v = CV x v

appendElem :: AnyVect -> IO AnyVect
appendElem (AnyVect v) = do
    putStr "> "
    hFlush stdout
    x <- readLn

    return $ if x == 0 then AnyVect v else AnyVect $ vecAppend x v

main = do
    AnyVect v <- appendElem $ AnyVect ZV
    putStrLn $ show v

which works as expected. Then I decided to get rid of the unecessary AnyVect:

{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE Rank2Types                #-}

import System.IO (hFlush, stdout)

data Z
data S n

data Vect n where
    ZV :: Vect Z
    CV :: Int -> Vect n -> Vect (S n)

instance Show (Vect n) where
    show ZV = "Nil"
    show (CV x v) = show x ++ " : " ++ show v

vecAppend :: Int -> Vect n -> Vect (S n)
vecAppend x ZV = CV x ZV
vecAppend x v = CV x v

appendElem :: Vect n -> (forall n. Vect n -> a) -> IO a
appendElem v f = do
    putStr "> "
    hFlush stdout
    x <- readLn

    return $ if x == 0 then f v else f $ vecAppend x v

main = do
    appendElem ZV show >>= putStrLn

which works as well even I don't really like the way main is written.

Is there any other simpler/cleaner way to write it?

Answer 1

If you don't want to use the new TypeLits in GHC 7.8, you can still improve your code using DataKinds and a typical refactoring to separate the IO and pure code.

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

import System.IO (hFlush, stdout)

data Nat = Z | S Nat -- using DataKinds to promote Z and S to type level

-- don't restrict ourselves to only Vec of Int, we can be more general
data Vec (n :: Nat) a where
    Nil  :: Vec Z a
    Cons :: a -> Vec n a -> Vec (S n) a

instance Show a => Show (Vec n a) where
    show Nil = "Nil"
    show (Cons a v) = show a ++ " : " ++ show v

-- vecAppend in the OP, append is usually reserved for functions that
-- look like `Vec n a -> Vec m a -> Vec (n + m) a`
cons :: a -> Vec n a -> Vec (S n) a
cons = Cons

-- refactor the IO related code into a separate function
prompt :: IO Int
prompt = do
    putStr "> "
    hFlush stdout
    readLn

-- the "if 0 then ... else ..." could also be refactored into a separate 
-- function that takes a initial Vec as input
main = do
    x <- prompt
    if x == 0
    then print (Nil :: Vec Z Int)
    else print (cons x Nil)