Haskell: экзистенциальные типы и ввод-вывод

Отправлено на 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

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

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


haskell existential-type
person Cristiano Paris    schedule 08.09.2014    source источник
comment
Похоже, это было бы лучше для проверки кода?   -  person J. Abrahamson    schedule 08.09.2014
comment
Перекрестился с codereview (о котором я не знал, что он существует). Спасибо.   -  person Cristiano Paris    schedule 08.09.2014
comment
vecAppend = CV более прямой. Я бы также переименовал его в vecCons, так как добавление звучит так, как будто оно работает с двумя векторами.   -  person chi    schedule 08.09.2014

Ответы (1)


arrow_upward
1
arrow_downward

Если вы не хотите использовать новый 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)
person cdk    schedule 08.09.2014
comment
Это хорошо, но, вероятно, мой пример был плохим для того, что я на самом деле намеревался сделать. Чтобы найти лучший, я подумал об обратном векторе, переданном пользователем, но, похоже, я не могу написать обратную функцию в первую очередь. - person Cristiano Paris; 09.09.2014