在 Haskell 中使用类型级编程进行评估：组合类型会丢失吗？

Question

我想使用类型级编程混合已评估和未评估的术语。

我做了一个简单的例子，其中 Sum 不求值，而 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 的评估替换为 cmets 中的评估：

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