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

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

Я сделал простой пример, где 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 на оценку в комментариях дает:

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
   |                              ^^^^^^

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


haskell type-level-computation
person Pierre van de Laar    schedule 21.01.2019    source источник
comment
eval никогда не может вернуть ничего, кроме функции, которая оценивается как Term 'True. В вашем сопоставлении с образцом, что произойдет, если x будет TermList v? Я думаю, вы получаете противоречие, не позволяющее GHC вывести тип.   -  person Bob Dalgleish    schedule 21.01.2019
comment
Я вижу, что не так, но не вижу, как это исправить. Чтобы использовать eval для x, который имеет тип Term a (логический a является экзистенциальным), требуется, чтобы экземпляр Eval (Term a) находился в области видимости. Но у нас есть только Eval (Term 'True) и Eval (Term 'False) в области видимости.   -  person Potato44    schedule 22.01.2019

Ответы (1)


arrow_upward
0
arrow_downward

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

{-# 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
person Pierre van de Laar    schedule 22.01.2019