Как создать EDSL для лямбда-исчисления (или CoC) в Haskell? - PullRequest
Новая
       8

Как создать EDSL для лямбда-исчисления (или CoC) в Haskell?

0 голосов
/ 24 сентября 2019

Уже есть тонны DSL лямбда-исчисления или построения исчисления.Но как насчет Embedded DSL?

В Haskell EDSL должен писать в монадическом стиле.Кроме того, необходимо уменьшить грамматический шум. 


type Name = String
data Expr
  = Pi Name Expr Expr
  | Lam Name Expr Expr
  | App Expr Expr
  | Atom Name
  | ConstType
  | ConstKind
  deriving (Show)

data EDSL = undefined

-- id = \(xT : Type) (x : xT) -> x 
id :: EDSL
id = do
  xT <- lam ConstType
  x <- lam xT
  return x 

-- applyTwice = \(a : Type) -> \(f : a -> a) -> \(x : a) -> f (f x)
applyTwice :: EDSL
applyTwice = do
  a <- lam ConstType
  f <- lam (pi a >> return a)
  x <- lam a
  return f (f x)

eDSL2Expr :: EDSL -> Expr

Я нахожу, что это может быть довольно сложно при попытке настроить, как работает приложение из 2 выражений (т.е. App e1 e2) в EDSL.

Если это невозможно, возможно ли использовать нетипизированное лямбда-выражение?

...