Haskell AST с рекурсивными типами

Question

В настоящее время я пытаюсь построить решатель расчета лямбда-исчисления, и у меня есть небольшая проблема с построением AST. Термин лямбда-исчисление индуктивно определяется следующим образом:

1) Переменная

2) лямбда, переменная, точка, и лямбда-выражение.

3) Скобка, выражение лямбда, выражение лямбда и скобка.

То, что я хотел бы сделать (и на первый пробовал) заключается в следующем:

data Expr = 
    Variable 
    | Abstract Variable Expr 
    | Application Expr Expr 

Теперь, очевидно, это не работает, так как переменная не является типом, и реферата Variable Expr ожидает типов. Так что мой Hacky решение это должно иметь:

type Variable = String 

data Expr = 
    Atomic Variable 
    | Abstract Variable Expr 
    | Application Expr Expr 

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

Answer 1

Ваше первое решение - это просто ошибочное определение без смысла. Variable не является типом, это конструктор с нулевым значением. Вы не можете ссылаться на Variable в определении типа, так как вы не можете ссылаться на какое-либо значение, например True, False или 100.

Второе решение, по сути, прямой перевод чего-то мы могли бы написать в BNF:

var ::= <string> 
term ::= λ <var>. <term> | <term> <term> | <var> 

И, таким образом, нет ничего плохого.

Answer 2

То, что вы точно хотите, чтобы иметь некоторый тип как

data Expr 
    = Atomic Variable 
    | Abstract Expr Expr 
    | Application Expr Expr 

Но сдерживать первый Expr в Abstract конструктору быть только Atomic. В Haskell нет простого способа сделать это, потому что значение какого-либо типа может быть создано любым конструктором этого типа. Таким образом, единственный подход заключается в том, чтобы создать отдельный тип данных или тип псевдонима для существующего типа (например, ваш псевдоним типа Variable) и переместить в него всю общую логику. Ваше решение с Variable выглядит очень хорошо для меня.

Но. Вы можете использовать некоторые другие дополнительные функции в Haskell для достижения своей цели по-разному. Вы можете быть вдохновлены пакетом glambda, который использует GADT для создания типизированного лямбда-исчисления.Также смотрите ответ: https://stackoverflow.com/a/39931015/2900502

Я могу придумать следующее решение для достижения вам минимальные цели (если вы хотите, чтобы ограничить первый аргумент Abstract):

{-# LANGUAGE GADTs   #-} 
{-# LANGUAGE KindSignatures #-} 

data AtomicT 
data AbstractT 
data ApplicationT 

data Expr :: * -> * where 
    Atomic  :: String -> Expr AtomicT 
    Abstract :: Expr AtomicT -> Expr a -> Expr AbstractT 
    Application :: Expr a -> Expr b -> Expr ApplicationT 

И следующий пример работает отлично:

ex1 :: Expr AbstractT 
ex1 = Abstract (Atomic "x") (Atomic "x") 

Но этот пример не компилируется из-за несоответствия типа:

ex2 :: Expr AbstractT 
ex2 = Abstract ex1 ex1