Haskell: Пространственно Типы и IO

Question

Cross-posted at Code Review SE

В своих попытках ухватить экзистенциальные типы в Haskell я решил реализовать фиксированной длины типа вектор данных основанную на целых числах. Я использую ghc 7.8.3.

В частности, я хотел написать программу, которая запрашивает у пользователя возможное новое значение для добавления к вектору фиксированной длины, а затем отображает результирующий вектор.

Сначала я написал первую версию программы, как это:

{-# 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 

, который работает, как ожидалось. Тогда я решил избавиться от ненужного 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 

, который работает, а я даже не очень нравится, как основной написано.

Есть ли какой-нибудь другой более простой/чистый способ его написать?

Answer 1

Если вы не хотите использовать новый TypeLits в GHC 7.8, вы все равно сможете улучшить свой код, используя DataKinds и типичный рефакторинг для разделения IO и чистого кода.

{-# 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)