Parse Simply Typed Lambda Calculus into a GADT.

Read.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeOperators #-}

module Read where

-- https://gist.github.com/pedrominicz/175564ac5e5ff8c66ddf8adecae25c10 (simplified version)
-- https://github.com/goldfirere/glambda/blob/master/src/Language/Glambda/Check.hs
-- https://github.com/goldfirere/glambda/blob/master/src/Language/Glambda/Type.hs
-- https://stackoverflow.com/questions/11104536/how-to-parse-strings-to-syntax-tree-using-gadts

import Control.Monad.Reader

import Data.List (elemIndex)
import Data.Type.Equality

import Text.Parsec hiding (Empty, parse)

data Elem as a where
  EZ :: Elem (a:as) a
  ES :: Elem as a -> Elem (b:as) a

instance Show (Elem as a) where
  show EZ     = show 0
  show (ES x) = show (1 + read (show x))

data Expr as a where
  Ref :: Elem as a -> Expr as a
  Abs :: Expr (a:as) b -> Expr as (a -> b)
  App :: Expr as (a -> b) -> Expr as a -> Expr as b
  Num :: Integer -> Expr as Integer

deriving instance Show (Expr as a)

-- Eval

data Value a where
  Closure :: Env as -> Expr as (a -> b) -> Value (a -> b)
  Number  :: Integer -> Value Integer

deriving instance Show (Value a)

data Env as where
  Empty :: Env '[]
  Cons  :: Value a -> Env as -> Env (a:as)

deriving instance Show (Env as)

get :: Elem as a -> Env as -> Value a
get EZ (Cons x _)      = x
get (ES x) (Cons _ xs) = get x xs

eval :: Expr '[] a -> Value a
eval x = go Empty x
  where go :: Env as -> Expr as a -> Value a
        go env (Ref x)    = get x env
        go env (Abs x)    = Closure env (Abs x)
        go env (App x y)  = apply (go env x) (go env y)
        go _ (Num x)      = Number x

        apply :: Value (a -> b) -> Value a -> Value b
        apply (Closure env (Abs body)) x = go (Cons x env) body
        apply _ _ = undefined

-- Type & Type Singleton

data UExpr
  = URef Int
  | UAbs Type UExpr
  | UApp UExpr UExpr
  | UNum Integer
  deriving Show

data Type
  = Arrow Type Type
  | NumT
  deriving Show

data Sing a where
  SArrow :: Sing a -> Sing b -> Sing (a -> b)
  SNum   :: Sing Integer

data Context as where
  Empty' :: Context '[]
  Cons'  :: Sing a -> Context as -> Context (a:as)

sing :: Type -> (forall a. Sing a -> b) -> b
sing (Arrow x y) k =
  sing x $ \x ->
  sing y $ \y ->
    k (SArrow x y)
sing NumT k = k SNum

eq :: Sing a -> Sing b -> Maybe (a :~: b)
eq (SArrow x x') (SArrow y y')
  | Just Refl <- eq x y
  , Just Refl <- eq x' y' = Just Refl
eq SNum SNum = Just Refl
eq _ _       = Nothing

-- Type Checker

check :: UExpr -> (forall a. Expr '[] a -> Maybe b) -> Maybe b
check expr k = go Empty' expr $ const k
  where go :: Context as -> UExpr -> (forall a. Sing a -> Expr as a -> Maybe b) -> Maybe b
        go ctx (URef x) k = getType ctx x $ \t x -> k t (Ref x)
        go ctx (UAbs t x) k =
          sing t $ \t ->
            go (Cons' t ctx) x $ \t' x ->
              k (SArrow t t') (Abs x)
        go ctx (UApp x y) k =
          go ctx x $ \tx x ->
          go ctx y $ \ty y ->
            case (tx, ty) of
              (SArrow ty t, ty') | Just Refl <- eq ty ty' ->
                k t (App x y)
              _ -> Nothing
        go _ (UNum x) k = k SNum (Num x)

getType :: Context as -> Int -> (forall a. Sing a -> Elem as a -> Maybe b) -> Maybe b
getType (Cons' x _) 0 k  = k x EZ
getType (Cons' _ xs) x k = getType xs (x - 1) $ \t x -> k t (ES x)
getType Empty' _ _ = undefined

-- Parser

type Parser = ParsecT String () (Reader [String])

parse :: String -> Maybe UExpr
parse s =
  case runReader (runParserT (whitespace *> expression <* eof) () "" s) [] of
    Left _  -> Nothing
    Right x -> Just x

expression :: Parser UExpr
expression = lambda
         <|> application

lambda :: Parser UExpr
lambda = do
  try $ char '\\' *> whitespace
  x <- name
  char ':' *> whitespace
  t <- lambdaType
  char '.' *> whitespace
  y <- local (x:) expression
  return $ UAbs t y

lambdaType :: Parser Type
lambdaType = ty `chainl1` arrow
  where ty = string "Num" *> whitespace *> return NumT <|> parens lambdaType
        arrow = string "->" *> whitespace *> return Arrow

application :: Parser UExpr
application = expression' `chainl1` return UApp
  where expression' = variable
                  <|> number
                  <|> parens expression

variable :: Parser UExpr
variable = do
  x   <- name
  env <- ask
  case elemIndex x env of
    Just x  -> return $ URef x
    Nothing -> fail ""

number :: Parser UExpr
number = try $ do
  sign   <- option ' ' (char '-')
  digits <- many1 digit
  whitespace
  return $ UNum (read (sign:digits))

name :: Parser String
name = do
  c  <- letter
  cs <- many alphaNum
  whitespace
  return (c:cs)

parens :: Parser a -> Parser a
parens p = between open close p
  where open  = char '(' <* whitespace
        close = char ')' <* whitespace

whitespace :: Parser ()
whitespace = skipMany space

-- Main

run :: String -> Maybe String
run expr = do
  expr <- parse expr
  result <- check expr $ Just . show . eval
  return result

main :: IO ()
main = do
  expr <- getLine
  case run expr of
    Just x  -> putStrLn x
    Nothing -> putStrLn "?"
  main