В Haskell, как разобрать нетипизированный АСТ на типизированный, основанный на GADT?

Question

Я пишу доменный язык в Haskell и установил на дизайн с двумя АСТ: исходный нетипичный, который представляет синтаксис, и окончательный типизированный, который представляет все. Я пишу последний как GADT, чтобы получить лучшую проверку типов.

Я думаю, что это почти работает, но у меня возникают проблемы писать функцию, которая преобразует начальное -> конечные (проверки типов, а также некоторые другие вещи, не показано, как все ссылки соответствуют переменной).

Вот упрощенный пример:

{-# LANGUAGE GADTs, StandaloneDeriving #-} 

module Main where 

-- untyped initial AST 

data Untyped 
    = UNum Int 
    | UStr String 
    | UAdd Untyped Untyped 
    deriving (Show, Eq) 

-- typed final AST 

data Typed a where 
    TNum :: Int -> Typed Int 
    TStr :: String -> Typed String 
    TAdd :: Typed Int -> Typed Int -> Typed Int 

deriving instance Eq (Typed a) 
deriving instance Show (Typed a) 

-- wrapper that allows working with a `Typed a` for any `a` 
data TypedExpr where 
    TypedExpr :: Typed a -> TypedExpr 

И это моя попытка функции check. Базовые случаи просты:

check :: Untyped -> Either String TypedExpr 
check (UNum n) = Right $ TypedExpr $ TNum n 
check (UStr s) = Right $ TypedExpr $ TStr s 
-- check (Uadd e1 e2) = ??? 

Но как я могу добавить Add? Он может рекурсивно оценить вложенные выражения для значений типа Either String (TypedExpr (Typed a)), но я не сумел разворачивать те, убедитесь, что типы выстраиваться (оба a s должна быть Int s), и повторно компресс позже. Я планировал сделать это все с матчей большой картины, но GHC не одобряет:

My brain just exploded 
    I can't handle pattern bindings for existential or GADT data constructors. 
    Instead, use a case-expression, or do-notation, to unpack the constructor. 

Вот объяснил here, но я не понял объяснения. Кажется Я не хочу сопоставлять образцы.

Обновление: Я, должно быть, испортил что-то еще, не заметив. Работа с шаблонами, как показывает Никита.

Таким образом, я возился вокруг, пытаясь заставить вещи в правильной форме, но еще ничего не получил. Если бы это были только Either String SomeValue Я бы хотел использовать аппликации, не так ли? Возможно ли добавить еще один уровень развертывания + тип проверки на них? Я подозреваю, что this answer близок к тому, что я хочу, так как вопрос очень похож, но опять я его не понимаю. This также могут быть связаны.

Обновление: That first answer - это то, что я хотел в конце концов. Но я не мог видеть, как до того, как Чи написал промежуточную версию ниже без дополнительного Type. Вот рабочее решение. Хитрость в том, чтобы пометить TypedExpr с с новым типом, представляющим только обратного типа (a) в виде Typed a:

data Returns a where 
    RNum :: Returns Int 
    RStr :: Returns String 

-- extend TypedExpr to include the return type 
data TypedExpr2 where 
    TypedExpr2 :: Returns a -> Typed a -> TypedExpr2 

Таким образом check не должен знать, является ли каждая Подвыражение является сырьевым TNum или функция (как Add), которая возвращает TNum:

check :: Untyped -> Either String TypedExpr2 
check (UNum n) = Right $ TypedExpr2 RNum (TNum n) 
check (UStr s) = Right $ TypedExpr2 RStr (TStr s) 
check (UAdd u1 u2) = do 
    -- typecheck subexpressions, then unwrap by pattern matching 
    TypedExpr2 r1 t1 <- check u1 
    TypedExpr2 r2 t2 <- check u2 
    -- check the tags to find out their return types 
    case (r1, r2) of 
    -- if correct, create an overall expression tagged with its return type 
    (RNum, RNum) -> return $ TypedExpr2 RNum $ TAdd t1 t2 
    _ -> Left "type error" 

GHC достаточно умен, чтобы знать, что два a s в любой TypedExpr2 должен совпадать, , чтобы он поймал вас, если вы попытаетесь использовать неправильный общий тип возврата на конце . Замечательно!

Answer 1

Технически это is выполнимо, но это довольно неудобно: вам нужно «копать» до тех пор, пока не будет найден конструктор GADT.

check :: Untyped -> Either String TypedExpr 
check (UNum n) = return $ TypedExpr $ TNum n 
check (UStr s) = return $ TypedExpr $ TStr s 
check (UAdd t1 t2) = do 
    t1 <- check t1 
    t2 <- check t2 
    case (t1, t2) of 
     (TypedExpr (TNum x)  , TypedExpr (TNum y)) 
     -> return $ TypedExpr $ TAdd (TNum x ) (TNum y) 
     (TypedExpr (TAdd x1 x2) , TypedExpr (TNum y)) 
     -> return $ TypedExpr $ TAdd (TAdd x1 x2) (TNum y) 
     (TypedExpr (TNum x)  , TypedExpr (TAdd y1 y2)) 
     -> return $ TypedExpr $ TAdd (TNum x ) (TAdd y1 y2) 
     (TypedExpr (TAdd x1 x2) , TypedExpr (TAdd y1 y2)) 
     -> return $ TypedExpr $ TAdd (TAdd x1 x2) (TAdd y1 y2) 
     _ -> Left "type error" 

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

Answer 2

Ваш точный вопрос легко отвечает следующим раствором:

check (UAdd (UNum a) (UNum b)) = Right $ TypedExpr $ TAdd (TNum a) (TNum b) 

Однако есть немало признаков дизайна лабиринта там.

Вы понимаете, что как только вы положили что-то в TypedExpr, вы потеряли всю информацию о a типа? Это делает вашу функцию check совершенно бессмысленной.

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

Я не понимаю, почему UAdd конструктор более Untyped значения, а Int, и я не понимаю, что заставило вас пойти с этой многоступенчатой ​​стратегии АСТ.

Я мог бы продолжать, но я сломаюсь здесь и просто рекомендую вам перепроектировать вашу модель.

Answer 3

Моя рекомендация будет использовать «обычный» представление вашей вселенной типов (с типом интерпретации функции), а затем сохранить Sing leton материализации своего экзистенциального типа в TypedExpr, то есть что-то вроде

{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies #-} 

data Type = TInt | TString 

type family InterpT (a :: Type) where 
    InterpT TInt = Int 
    InterpT TString = String 

-- plus the usual singletons stuff 
-- ... 

-- and finally 
data Typed (a :: Type) where ... 

data TypedExpr where 
    TypedExpr :: Sing a -> Typed a -> TypedExpr 

Таким образом, вы можете сделать что-то вроде

check (UAdd e1 e2) = do 
    TypedExpr t1 e1' <- check e1 
    TypedExpr t2 e2' <- check e2 
    case testEquality t1 t2 of 
    Just Refl -> ... use e1' and e2' here, you know they have the same Type 
    Nothing -> Left ... 

Найти полностью плотское обличие примера here.