Оценка с использованием программирования на уровне типов в Haskell: теряются ли составные типы?

Question

Я хотел бы смешать оцененные и неоцененные термины, используя программирование на уровне типов.

Я сделал простой пример, в котором сумма не оценивается, а Const оценивается.

Отлично работает следующее:

{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE TypeFamilies        #-}
{-# LANGUAGE FlexibleInstances   #-}
module Main where

type family And a b where
    And 'True 'True = 'True
    And _     _     = 'False

data TermList (b::Bool) where
    Nil :: TermList 'True
    Cons :: Term a -> TermList b -> TermList (And a b)

instance Show (TermList b) where
    show Nil = "Nil"
    show (Cons a b) = "(Cons " ++ show a ++ " " ++ show b ++ ")"

data Term (b::Bool) where
    Const :: Int -> Term 'True
    Sum  :: TermList v -> Term 'False

instance Show (Term b) where
    show (Const a) = "(Const " ++ show a ++ ")"
    show (Sum a) = "(Sum " ++ show a ++ ")"

class Eval e where
    eval :: e -> Term 'True

instance Eval (Term 'True) where
    eval = id

instance Eval (Term 'False) where
    eval (Sum x)    = eval x

instance Eval (TermList b) where
    eval _ = Const 0

{-
instance Eval (TermList b) where
    eval (Nil)       = Const 0
    eval (Cons x xs) = case (eval x, eval xs) of
                            (Const v, Const vs) -> Const (v + vs)
-}

main :: IO ()
main = 
    let sum1 = Sum (Cons (Const 3) (Cons (Const 4) Nil))
        sum2 = Sum (Cons (Const 5) (Cons (Const 6) Nil))
        sum3 = Sum (Cons sum1 (Cons sum2 Nil))
    in
        do
            putStrLn (show sum1)
            putStrLn (show sum2)
            putStrLn (show sum3)

            putStrLn (show (eval sum1))
            putStrLn (show (eval sum2))
            putStrLn (show (eval sum3))

Тем не менее, замена оценки TermList на оценку в комментариях дает:

src\Main.hs:45:30: error:
    * Could not deduce (Eval (Term a)) arising from a use of `eval'
      from the context: b ~ And a b1
        bound by a pattern with constructor:
                   Cons :: forall (a :: Bool) (b :: Bool).
                           Term a -> TermList b -> TermList (And a b),
                 in an equation for `eval'
        at src\Main.hs:45:11-19
    * In the expression: eval x
      In the expression: (eval x, eval xs)
      In the expression:
        case (eval x, eval xs) of { (Const v, Const vs) -> Const (v + vs) }
   |
45 |     eval (Cons x xs) = case (eval x, eval xs) of
   |                              ^^^^^^

Это действительно удивляет меня: должны ли помнить типы всех составных частей?

Answer 1

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

{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE TypeOperators       #-}
{-# LANGUAGE TypeFamilies        #-}
{-# LANGUAGE FlexibleInstances   #-}
module Main where

data Term (b::Bool) where
    Const :: Int -> Term 'True
    Sum  :: -- Need to add constraints, yet they could be derived by the compiler
            (Show (TermList v), Eval (TermList v)) => TermList v -> Term 'False

instance Show (Term b) where
    show (Const a) = "(Const " ++ show a ++ ")"
    show (Sum a) = "(Sum " ++ show a ++ ")"

instance Eq (Term 'True) where
    Const a == Const b = a==b

data TermList (xs :: [ Bool ]) where
    TNil :: TermList '[]
    TCons :: Term x -> TermList xs -> TermList (x ': xs)

instance Show (TermList '[]) where
    show TNil = "Nil"

instance Show (TermList xs) => Show (TermList (x ': xs)) where
    show (TCons a b) = "(Cons " ++ show a ++ " " ++ show b ++ ")"

class Eval e where
    eval :: e -> Term 'True

instance Eval (Term 'True) where
    eval = id

instance Eval (Term 'False) where
    eval (Sum x)    = eval x

instance Eval (TermList '[]) where
    eval TNil        = Const 0

-- need to add Eval (Term x), yet Eval (Term 'True) and Eval (Term 'False) are provided!
instance (Eval (Term x), Eval (TermList xs)) => Eval (TermList (x ': xs)) where
    eval (TCons x xs) = case (eval x, eval xs) of
                             (Const v, Const vs) -> Const (v + vs)

main :: IO ()
main = let sum1  = Sum (TCons (Const 3) (TCons (Const 4) TNil))
           sum2  = Sum (TCons (Const 5) (TCons (Const 6) TNil))
           sum12 = Sum (TCons sum1      (TCons sum2      TNil))

           sumEval12 = Sum (TCons (eval sum1)      (TCons (eval sum2)      TNil))
        in do
            putStrLn (show sum1)
            putStrLn (show sum2)
            putStrLn (show sum12)

            putStrLn (show (eval sum1))
            putStrLn (show (eval sum2))
            putStrLn (show (eval sum12))

            putStrLn (show sumEval12)
            putStrLn (show (eval sumEval12 == eval sum12))

выполнение этого программирования дает ожидаемый результат

(Sum (Cons (Const 3) (Cons (Const 4) Nil)))
(Sum (Cons (Const 5) (Cons (Const 6) Nil)))
(Sum (Cons (Sum (Cons (Const 3) (Cons (Const 4) Nil))) (Cons (Sum (Cons (Const 5) (Cons (Const 6) Nil))) Nil)))
(Const 7)
(Const 11)
(Const 18)
(Sum (Cons (Const 7) (Cons (Const 11) Nil)))
True