Henlo

Main.hs

@@ -0,0 +1,203 @@
+module Main(main) where
+
+import Data.List ((\\), union)
+import Control.Monad (when, foldM_)
+import System.Environment (getArgs)
+import Parser
+
+data TopLevel
+    = Declaration String Expr
+    | Definition String Expr
+    | Comment String
+instance Show TopLevel where
+    show (Declaration name value) = name ++ " : " ++ show value
+    show (Definition name value) = name ++ " = " ++ show value
+    show (Comment content) = "-- " ++ content
+
+data Expr
+    = Abs String Expr Expr
+    | App Expr Expr
+    | Var String
+    | Pi String Expr Expr
+    | Kind Kinds
+    deriving (Eq)
+instance Show Expr where
+    show (Abs param type_ body) = "\\" ++ param ++ ": " ++ show type_ ++ "." ++ show body
+    show (App (Var name) (Var name')) = name ++ " " ++ name'
+    show (App func (Var name)) = show func ++ " " ++ name
+    show (App (Var name) arg) = name ++ " " ++ "(" ++ show arg ++ ")"
+    show (App func arg) = "(" ++ show func ++ ")" ++ " " ++ "(" ++ show arg ++ ")"
+    show (Var name) = name
+    show (Kind k) = show k
+    show (Pi name value body) = "(" ++ name ++ ": " ++ show value ++ ") -> " ++ show body
+
+data Kinds = Star | Box deriving (Eq)
+instance Show Kinds where
+    show Star = "*"
+    show Box = "☐"
+
+-- Parser
+
+exprP, absP, piP, appP, varP, kindP, arrowP :: Parser Expr
+absP =  Abs
+    <$> ((charP 'λ' <|> charP '\\') *> wordP <* charP ':')
+    <*> (exprP <* charP '.')
+    <*> exprP
+piP =  Pi
+   <$> (charP '(' *> wordP <* charP ':')
+   <*> (exprP <* charP ')')
+   <*> (stringP "->" *> (piP <|> arrowP <|> exprP))
+arrowP = do
+    let exprP' = (arrowP <|> absP <|> piP <|> kindP <|> appP <|> varP)
+    from <- ((absP <|> piP <|> kindP <|> appP <|> varP) <* stringP "->")
+    to <- exprP'
+    return $ Pi "_" from to
+varP = Var <$> wordP
+kindP = Kind Star <$ charP '*'
+appP = do
+    let exprP' = (charP '(' *> appP <* charP ')') <|> absP <|> piP <|> kindP <|> varP <|> arrowP
+    head <- exprP'
+    tail <- some (charP ' ' *> exprP')
+    return $ foldl App head tail
+exprP = piP <|> arrowP <|> appP <|> absP <|> kindP <|> varP
+
+topLevelP, declP, defnP, commP :: Parser TopLevel
+declP =  Declaration
+     <$> wordP <* charP ':'
+     <*> exprP
+defnP =  Definition
+     <$> wordP <* charP '='
+     <*> exprP
+commP = Comment <$> (stringP "--" *> many (predP (/= '\n')))
+topLevelP = (declP <|> defnP <|> commP) <* many spaceP
+
+-- Normalisation
+
+newSymbol :: String -> [String] -> String
+newSymbol param free
+    | param `elem` free = newSymbol (param ++ "'") free
+    | otherwise = param
+
+freeVars :: Expr -> [String]
+freeVars (Var name) = [name]
+freeVars (App func arg) = freeVars func `union` freeVars arg
+freeVars (Abs param _ body) = freeVars body \\ [param]
+freeVars (Pi name value body) = freeVars value `union` freeVars body \\ [name]
+freeVars (Kind _) = []
+
+subst :: String -> Expr -> Expr -> Expr
+subst var for abs@(Abs param type_ body)
+    | param == var = abs
+    | param `elem` freeVars for = 
+        let param' = newSymbol param (freeVars for `union` freeVars body)
+            body'  = subst param (Var param') body
+         in Abs param' type_ (subst var for body')
+    | otherwise = Abs param type_ (subst var for body)
+subst var for (App func arg) = App (rec func) (rec arg)
+    where rec = subst var for
+subst var for (Var name)
+    | var == name = for
+    | otherwise   = Var name
+subst var for (Kind k) = Kind k
+subst var for pi@(Pi param value body)
+    | param == var = pi
+    | param `elem` freeVars for = 
+        let param' = newSymbol param (freeVars for `union` freeVars body)
+            body'  = subst param (Var param') body
+         in Pi param' (subst var for value) (subst var for body')
+    | otherwise = Pi param (subst var for value) (subst var for body)
+
+alphaEq :: Expr -> Expr -> Bool
+alphaEq (Var name) (Var name') = name == name'
+alphaEq (App func arg) (App func' arg') = alphaEq func func' && alphaEq arg arg'
+alphaEq (Abs param type_ body) (Abs param' type_' body') =
+    alphaEq type_ type_' && alphaEq body (subst param' (Var param) body')
+alphaEq (Kind k) (Kind k') = k == k'
+alphaEq (Pi param value body) (Pi param' value' body') =
+    alphaEq body (subst param' (Var param) body') && alphaEq value value'
+alphaEq _ _ = False
+
+nf :: Expr -> Expr
+nf (App func arg) = case nf func of
+    Abs param _ body ->
+        let arg' = nf arg
+         in nf (subst param arg' body)
+    Pi name value body ->
+        let arg' = nf arg
+         in nf (subst name arg' body)
+    func' -> App func' (nf arg)
+nf (Abs param type_ body) = Abs param type_ (nf body)
+nf (Pi name value body) = Pi name (nf value) (nf body)
+nf expr = expr
+
+betaEq :: Expr -> Expr -> Bool
+betaEq a b = alphaEq (nf a) (nf b)
+
+-- Type checking
+
+newtype Env = Env [(String, Expr)] deriving Show
+instance Semigroup Env where
+    Env a <> Env b = Env $ union a b
+instance Monoid Env where
+    mempty = Env []
+extend :: Env -> String -> Expr -> Env
+extend (Env env) name type_ = Env $ (name, type_) : env
+
+findVar :: Env -> String -> Either String Expr
+findVar (Env env) key = maybe (Left $ "Cannot find variable " ++ key) Right $ lookup key env
+
+allowedKinds :: [(Expr, Expr)]
+allowedKinds = [(Kind Star, Kind Star), (Kind Star, Kind Box), (Kind Box, Kind Star), (Kind Box, Kind Box)]
+
+typeCheck :: Env -> Expr -> Either String Expr
+typeCheck env (Var name) = findVar env name
+typeCheck env (Abs param type_ body) = do
+    typeCheck env type_
+    retT <- typeCheck (extend env param type_) body
+    let funcT = Pi param type_ retT
+    typeCheck env funcT
+    return funcT
+typeCheck env (Kind Star) = return (Kind Box)
+typeCheck env (Kind Box)  = Left "Found a box"
+typeCheck env (Pi name value body) = do
+    valueT <- typeCheck env value
+    bodyT <- typeCheck (extend env name value) body
+    when ((valueT, bodyT) `notElem` allowedKinds) $ Left $
+        "bad abstraction: " ++ show valueT ++ " and " ++ show bodyT 
+    return bodyT
+typeCheck env (App func arg) = do
+    funcT <- typeCheck env func
+    case funcT of
+        Pi name value body -> do
+            argT <- typeCheck env arg
+            when (not $ betaEq value argT) $
+                Left $ "Cannot match types for function call: " ++ show value ++ " and " ++ show argT
+            return $ subst name arg body
+        _ -> Left "Calling a non-function"
+
+typeCheckTopLevel :: Env -> TopLevel -> Either String Env
+typeCheckTopLevel env (Declaration name value) = do
+    valueT <- typeCheck env value
+    return (extend env name value)
+typeCheckTopLevel env (Definition name value) = do
+    valueT <- typeCheck env value
+    case findVar env name of
+        Right type_ -> do
+            when (not $ betaEq valueT type_) $ Left $
+                "Mismatched types between declaration and definition: " ++ show valueT ++ " and " ++ show type_
+            return env
+        Left _ -> return (extend env name valueT)
+
+-- Interaction
+
+main :: IO ()
+main = do
+    [filename] <- getArgs 
+    source <- readFile filename
+    case runParser (some topLevelP) source of
+        Just (program, []) -> 
+            case foldM_ typeCheckTopLevel mempty program of
+                Right ty -> putStrLn "done."
+                Left err -> putStrLn err 
+        Just (_, rest) -> putStrLn $ "Parse error at " ++ rest
+        Nothing -> putStrLn "Parse error"

Parser.hs

@@ -0,0 +1,81 @@
+{-# LANGUAGE LambdaCase #-}
+
+module Parser 
+    ( module Parser
+    , module Control.Applicative
+    ) where
+
+import Control.Applicative
+import Data.Char
+import Debug.Trace
+
+newtype Parser a = Parser { runParser :: String -> Maybe (a, String) }
+instance Functor Parser where
+    fmap f (Parser p) = Parser $ \input -> do
+        (value, rest) <- p input
+        return (f value, rest)
+
+instance Applicative Parser where
+    pure a = Parser $ \input -> Just (a, input)
+    (Parser f) <*> (Parser g) = Parser $ \input -> do
+        (fn, rest) <- f input
+        (value, rest') <- g rest
+        return (fn value, rest')
+
+instance Monad Parser where
+    return = pure
+    (Parser a) >>= f = Parser $ \input -> do
+        (value, rest) <- a input
+        let Parser b = f value
+         in b rest
+
+instance Alternative Parser where
+    empty = Parser $ const Nothing
+    (Parser a) <|> (Parser b) = Parser $ \input -> a input <|> b input
+
+instance MonadFail Parser where
+    fail s = Parser $ const Nothing
+
+charP :: Char -> Parser Char
+charP c = Parser $ \case
+    [] -> Nothing
+    (x : xs)
+        | x == c -> Just (c, xs)
+        | otherwise -> Nothing
+
+stringP :: String -> Parser String
+stringP = sequence . map charP
+
+predP :: (Char -> Bool) -> Parser Char
+predP pred = Parser $ \case
+    [] -> Nothing
+    (x : xs)
+        | pred x -> Just (x, xs)
+        | otherwise -> Nothing
+
+digitP :: Parser Char
+digitP = predP isDigit
+
+numberP :: Parser Int
+numberP = read <$> some digitP
+
+letterP :: Parser Char
+letterP = predP (`notElem` [':','\\', 'λ', '.', ' ', '-', '>', '*', '(', ')', '=', '\n'])
+
+wordP :: Parser String
+wordP = some letterP
+
+spaceP :: Parser ()
+spaceP = () <$ predP isSpace
+
+notFollowedBy :: Parser a -> Parser b -> Parser a
+a `notFollowedBy` b = Parser $ \input -> do
+    (value, rest) <- runParser a input
+    case runParser b rest of
+        Just _ -> Nothing
+        Nothing -> Just (value, rest)
+
+debug :: Show a => Parser a -> Parser a
+debug p = Parser $ \input -> case runParser p input of
+    ret@(Just (value, rest)) -> trace ("Input: " ++ input ++ "\nParsed: " ++ show value ++ "\nRest: " ++ rest ++ " (" ++ show (length rest) ++ ")") ret
+    Nothing -> trace ("Input: " ++ input) Nothing

grammar.ebnf

@@ -0,0 +1,10 @@
+top-level ::= ident ':' expr
+            | ident '=' expr
+            | '--' text
+
+expr ::= ('\' | 'λ') ident ':' expr '.' expr
+       | expr expr
+       | '(' ident ':' expr ')' '->' expr
+       | '(' expr ')' '->' expr
+       | '*'
+       | ident

test.lc

@@ -0,0 +1,10 @@
+N:*
+0:N
+S:N->N
+
+Vect:N->*->*
+nil:(a:*)->Vect 0 a
+cons:(a:*)->(n:N)->a->Vect n a->Vect (S n) a
+
+testvec:Vect (S 0) N
+testvec=cons N (S 0) 0 (cons N 0 (S 0) (nil N))