Блог

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

Попытка определить функцию, которая позволяет узнать тип, который имеет параметр.

Это язык:

 data Ty = Ty :-> Ty | INT  deriving (Eq,Show)
infixr 9 :->
data Expr = Var Nm  | Lam (Nm,Ty) Expr | App Expr Expr
      | Val Int | Add Expr Expr | If Expr Expr Expr
      | Let Nm Expr Expr
      | Rec Expr        deriving Show
type Nm = String
 

И это оценщик до сих пор:

 type Te = [ (Nm, Ty) ]
type En = [ (Nm, Value) ]

ty :: Te -> Expr -> Ty
ty te (Var x) = lookup' x te
ty te (Lam (x,t) e) = t :-> t2
  where
    t2 = ty ((x,t):te) e
ty te (App e1 e2) =
  case t1 of
    t2' :-> t  | t2==t2'   -> t
               | otherwise -> error $ show e1    show e2
    _ -> error $ show "not a function type"
  where
    t1 = ty te e1
    t2 = ty te e2
ty te (Val _) = INT
ty te (Add e1 e2) =
  case (t1, t2) of
    (INT, INT) -> INT
    (INT, _  ) -> error $ show "is not INT type"
    _          -> error $ show e1    "is not INT type"
  where
    t1 = ty te e1
    t2 = ty te e2
ty te (If e e1 e0) =
  case t of
    INT | t1 == t0  -> t1
        | otherwise -> error $ show "different type"
    _ -> error $ show e    "is not INT type"
  where
    t = ty te e
    t1 = ty te e1
    t0 = ty te e0
ty en (Let x e1 e2) = ty ((x,t2) : en) e2
                            where
                                t2 = ty en e1
ty te e = error $ show e    "type inference is not defined yet"
lookup' x en = case lookup x en of
                  Nothing -> error (x    " not defined")
                  Just v  -> v
 

Например, тест типа let :

 t1 = Let "z" (Val 1) (Add (Var "z") (Val 2))

ty [] t1
 

ответ: INT

rec выражение используется для определения рекурсивной функции

Это моя тестовая функция, которую я хочу оценить:

 t2 = Rec  (Lam ("f", INT :-> INT) . Lam ("i", INT) $
                If (Var "i")
                    (Var "i" `Add` (App (Var "f") (Var "i" `Add` Val(-1))))
                    (Var "i")     
            )
ty [] t2
 

Я пытался сделать выражение:

 ty en (Rec (Lam (x,_) e)) = v
                where 
                    v = ty ((x,v):en) e
 

Rec пробовал тест типа like let , но есть ошибка.

Я уже реализовывал подобный код в прошлом, так что вам следует обратиться к нему. Вам не нужно обращать внимания на наличие лицензии (ЛИЦЕНЗИЯ все объясняет).

Rec символ не нужен для определения рекурсивной функции. Если Let и Var работают правильно, вы можете определить. Пример, приведенный выше, касается среды для каждой области действия функции, но даже если он будет работать только с глобальной средой, он будет работать.

Для определения типов Let здесь. Здесь, учитывая взаимную рекурсивную функцию, поэтому используйте модуль graph, но сейчас не обращайте на это внимания. Имя, привязанное к Let нему, может принимать несколько выражений, хотя так же хорошо, как и одно.

Тогда inferBinds это было бы просто. Он принимает Name и Expr ( Maybe Type для аннотации типа, поэтому может забыть его) и возвращает Type with [Constraint] (они входят в комплект as Answer ). Вот как собирать ограничения.

После того, как вы получите ограничения, это так просто. См solve . раздел Функция. Здесь solve тип переменных определяется рекурсивно с помощью ограничений. См . Также unify и bind .

Мне действительно нужно написать о подстановке, новых переменных и так далее, Но я слишком устал, чтобы объяснять дальше. Если вы хотите узнать подробнее, настоятельно рекомендую ознакомиться с типами и языками программирования.