Использование Fold-интерпретатора на GADT

Question

Несколько недель назад я прочитал " Написание переводчика", используя фолд. Я пытался применить этот метод к проекту, над которым я работаю, но были ошибки из-за GADT. Вот игрушечный код, который генерирует ту же проблему.

{-# LANGUAGE GADTs, KindSignatures #-} 


data Expr :: * -> * where
    Val  :: n ->                Expr n
    Plus :: Expr n -> Expr n -> Expr n

data Alg :: * -> * where
    Alg :: (n ->      a) 
        -> (a -> a -> a) 
        -> Alg a

fold :: Alg a -> Expr n -> a
fold alg@(Alg val _) (Val n) = val n
fold alg@(Alg _ plus) (Plus n1 n2) = plus (fold alg n1) (fold alg n2)

Вот сообщение об ошибке.

/home/mossid/Code/Temforai/src/Temforai/Example.hs:16:36: error:
    • Couldn't match expected type ‘n1’ with actual type ‘n’
      ‘n’ is a rigid type variable bound by
        the type signature for:
          fold :: forall a n. Alg a -> Expr n -> a
        at /home/mossid/Code/Temforai/src/Temforai/Example.hs:15:9
      ‘n1’ is a rigid type variable bound by
        a pattern with constructor:
          Alg :: forall a n. (n -> a) -> (a -> a -> a) -> Alg a,
        in an equation for ‘fold’
        at /home/mossid/Code/Temforai/src/Temforai/Example.hs:16:11
    • In the first argument of ‘val’, namely ‘n’
      In the expression: val n
      In an equation for ‘fold’: fold alg@(Alg val _) (Val n) = val n
    • Relevant bindings include
        n :: n
          (bound at /home/mossid/Code/Temforai/src/Temforai/Example.hs:16:27)
        val :: n1 -> a
          (bound at /home/mossid/Code/Temforai/src/Temforai/Example.hs:16:15)
        fold :: Alg a -> Expr n -> a
          (bound at /home/mossid/Code/Temforai/src/Temforai/Example.hs:16:1)

Я думаю, что компилятор не может сделать вывод, что n а также n1 являются одними и теми же типами, поэтому ответом может быть поднятие внутренней переменной до сигнатуры типа данных. Однако, не так, как в этом примере, его нельзя использовать в исходном коде. В исходном коде есть переменная типа forall-quanified в Exprи подпись типа должна обрабатывать конкретную информацию.

+ Вот оригинальный код

data Form :: * -> * where
    Var     :: Form s
    Prim    :: (Sat s r) => Pred s -> Marker r          -> Form s
    Simple  :: (Sat s r) => Pred s -> Marker r          -> Form s
    Derived ::              Form r -> Suffix r s        -> Form s
    Complex :: (Sat s r, Sat t P) => 
                            Form s -> Infix r -> Form t -> Form s

data FormA a where
    FormA :: (Pred s -> Marker t -> a) 
          -> (Pred u -> Marker v -> a)
          -> (a -> Suffix w x    -> a)
          -> (a -> y -> a        -> a)
          -> FormA a

foldForm :: FormA a -> Form s -> a
foldForm alg@(FormA prim _ _ _) (Prim p m) = prim p m
foldForm alg@(FormA _ simple _ _) (Simple p m) = simple p m
foldForm alg@(FormA _ _ derived _) (Derived f s) = 
    derived (foldForm alg f) s
foldForm alg@(FormA _ _ _ complex) (Complex f1 i f2) = 
    complex (foldForm alg f1) i (foldForm alg f2)

Answer 1

Для обеспечения n внутри Alg является правильным, вы можете представить его в качестве параметра для Alg Конструктор типов.

data Alg :: * -> * -> * where
    Alg :: (n ->      a) 
        -> (a -> a -> a) 
        -> Alg n a

fold :: Alg n a -> Expr n -> a
fold alg@(Alg val _) (Val n) = val n
fold alg@(Alg _ plus) (Plus n1 n2) = plus (fold alg n1) (fold alg n2)

в Form код, это выглядит сложнее. Там много экзистенциально-количественных переменных типа. Нужно найти способ выставить их всех в типе, чтобы они могли быть одинаковыми в Form а также FormA,