Skip to content

Instantly share code, notes, and snippets.

@srijs
Forked from chrisdone/AnIntro.md
Last active August 29, 2015 14:09
Show Gist options
  • Save srijs/94ee6a254e0b5b58a922 to your computer and use it in GitHub Desktop.
Save srijs/94ee6a254e0b5b58a922 to your computer and use it in GitHub Desktop.

Basic unit type:

λ> replTy "()"
() :: ()

Basic functions:

λ> replTy "(fn x x)"
(fn x x) :: b -> b

λ> replTy "((fn x ()) (fn x x))"
((fn x ()) (fn x x)) :: ()

λ> repl "((fn x x) (fn x x))"
((fn x x) (fn x x)) :: c -> c
(fn x x)

Statically typed:

λ> repl "(() (fn x x))"
-- *** Exception: Couldn't match expected type: ()
-- against type: (b -> b) -> e

Standard quotation:

λ> replTy "'()"
'() :: 'Symbol
λ> repl "'(foo bar)"
'(foo bar) :: 'Symbol
(foo bar)

Statically typed quotation:

λ> replTy "~()"
~() :: '()

All quotes have type 'a. Normal symbolic Lisp style is 'Symbol, quoting anything else, e.g. for unit, is '(). Also things have to be in scope:

λ> repl "~a"
-- *** Exception: Not in scope: `a'

Quoted function:

λ> replTy "'(fn x x)"
'(fn x x) :: 'Symbol

Quoted function:

λ> replTy "~(fn x x)"
~(fn x x) :: '(b -> b)

Notice the type is '(b -> b).

There's an eval function:

λ> replTy "eval"
eval :: 'a -> a

It accepts a quoted a and returns the a that it represents. It won't accept anything not quoted:

λ> replTy "(eval ())"
-- *** Exception: Couldn't match expected type: 'a
-- against type: ()

If given a symbolic quoted expression, it will just return it as-is:

λ> repl "(eval '())"
(eval '()) :: Symbol
()
λ> repl "(eval '((fn x x) '()))"
(eval '((fn x x) '())) :: Symbol
((fn x x) ())

Given a well-typed quoted expression it will run the code:

λ> repl "(eval ~((fn x x) '()))"
(eval ~((fn x x) '())) :: 'Symbol
()
λ> repl "(eval ~((fn x x) ()))"
(eval ~((fn x x) ())) :: ()
()
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE FlexibleContexts #-}
-- | Statically typed Lisp with typed quotation.
module Type where
import Control.Applicative
import Control.Arrow ((***))
import Control.Monad.State.Strict
import Control.Monad.Writer
import Data.Attoparsec.Text (Parser)
import qualified Data.Attoparsec.Text as P
import Data.Char
import Data.Map (Map)
import qualified Data.Map as M
import Data.Set (Set)
import qualified Data.Set as S
import Data.String
import Data.Text (Text)
import qualified Data.Text as T
import qualified Data.Text.IO as T
--------------------------------------------------------------------------------
-- Types
-- | A type.
data Type
= VarTy (Name Type)
| FunTy Type Type
| UnitTy
| SymbolTy
| QuotedTy Type
deriving (Ord,Eq,Show)
-- | An expression.
data Exp
= Var (Name Exp)
| Fun (Name Exp) Type Exp
| Unit
| App Exp Exp
| TypedQuote Exp
| Quote Exp
| Eval (Exp -> Exp)
-- | A name for some thing.
newtype Name a = Name Text
deriving (Ord,Eq,Show)
-- | A stream type.
data Stream a =
Stream a (Stream a)
--------------------------------------------------------------------------------
-- REPL
repl :: Text -> IO ()
repl inp =
case P.parseOnly (ex nameStream <* P.endOfInput)
inp of
Left err -> error err
Right (std -> expr,stream) ->
do T.putStrLn
(inp <> " :: " <>
prettyType (typeOf expr stream))
T.putStrLn
(prettyExp (eval expr))
replTy :: Text -> IO ()
replTy inp =
case P.parseOnly (ex nameStream <* P.endOfInput)
inp of
Left err -> error err
Right (std -> expr,stream) ->
T.putStrLn
(inp <> " :: " <>
prettyType (typeOf expr stream))
replCheck :: Text -> IO ()
replCheck inp =
case P.parseOnly (ex nameStream <* P.endOfInput)
inp of
Left err -> error err
Right (std -> expr,stream) ->
print ((prettyType ***
S.map (prettyType *** prettyType)) (evalState (check mempty expr) stream))
--------------------------------------------------------------------------------
-- Stdlib stuff
-- | Bind standard library things.
std :: Exp -> Exp
std e =
(App (Fun (Name "eval")
(FunTy (QuotedTy (VarTy "a"))
(VarTy "a"))
e)
(Eval eval))
--------------------------------------------------------------------------------
-- Parser
ex :: Stream (Name Type) -> Parser (Exp,Stream (Name Type))
ex ss = quote ss <|> tquote ss <|> app ss <|> fn ss <|> unit ss <|> var ss
where tquote s =
P.string "~" *>
fmap (\(x,s') -> (TypedQuote x,s'))
(ex s)
quote s =
P.string "'" *>
fmap (\(x,s') -> (Quote x,s'))
(ex s)
var s = fmap (\x -> (Var x,s)) ident
fn s =
do void (P.string "(fn ")
P.skipSpace
i <- ident
void P.space
P.skipSpace
(body,Stream n s') <- ex s
void (P.string ")")
return (Fun i (VarTy n) body,s')
app s =
do void (P.string "(")
(op,s') <- ex s
void P.space
P.skipSpace
(arg,s'') <- ex s'
void (P.string ")")
return (App op arg,s'')
unit s =
P.string "()" *>
pure (Unit,s)
ident :: Parser (Name a)
ident =
do c <- P.letter
cs <- P.takeWhile (\ch -> isLetter ch || isDigit ch)
return (Name (T.singleton c <> cs))
--------------------------------------------------------------------------------
-- Interpreter
-- | Eval expression.
eval :: Exp -> Exp
eval (App op arg) =
case eval op of
Eval f ->
case arg of
TypedQuote e -> eval e
Quote e -> e
_ ->
error "Can only eval things of type 'a."
Fun param _ expr ->
case eval arg of
a@Var{} ->
error (T.unpack (prettyExp a <> " is not in scope"))
a -> eval (subst param a expr)
_ ->
error (T.unpack (prettyExp op <> " is not a function"))
eval e@(Var{}) =
error (T.unpack (prettyExp e <> " is not in scope!"))
eval e = e
-- | Substitute name in function body.
subst :: Name Exp -> Exp -> Exp -> Exp
subst name val e@(Var name')
| name == name' = val
| otherwise = e
subst name val (Fun name' ty e)
| name /= name' = Fun name' ty (subst name val e)
subst name val (App f a) =
App (subst name val f) (subst name val a)
--
-- TODO: retain original name in quotes:
--
-- λ> repl "((fn f ~f) (fn a a))"
-- ((fn f ~f) (fn a a)) :: '(c -> c)
-- (fn a a)
--
-- This should really produce: f
-- But it doesn't due to dumb beta reduction.
--
subst name val (TypedQuote e) =
TypedQuote (subst name val e)
subst _ _ e = e
--------------------------------------------------------------------------------
-- Type checker
-- | Get the type of the expression.
typeOf :: Exp -> Stream (Name Type) -> Type
typeOf t stream =
case evalState (check mempty t) stream of
(ty,cs) -> let s = evalState (unify (S.toList cs)) ()
in replace s ty
-- | Check the exp with the given context.
check :: MonadState (Stream (Name Type)) m
=> Map (Name Exp) Type -> Exp -> m (Type,Set (Type,Type))
check ctx expr =
case expr of
Var name@(Name text) ->
case M.lookup name ctx of
Nothing ->
error ("Not in scope: `" <> T.unpack text <> "'")
Just typ -> return (typ,mempty)
Fun x xty body ->
do (rty,cs) <- check (M.insert x xty ctx) body
return (FunTy xty rty,cs)
Unit -> return (UnitTy,mempty)
App f x ->
do (fty,cs1) <- check ctx f
(xty,cs2) <- check ctx x
sym <- genSym
let rty = VarTy sym
cs =
S.insert (fty,FunTy xty rty)
(cs1 <> cs2)
return (rty,cs)
TypedQuote e ->
do (qty,cs) <- check ctx e
return (QuotedTy qty,cs)
Quote{} -> return (QuotedTy SymbolTy,mempty)
Eval _ ->
do ty <- genSym
return (VarTy ty,mempty)
-- | Unify the list of constraints.
unify :: Monad m => [(Type,Type)] -> m (Map (Name Type) Type)
unify [] = return mempty
unify ((a,b):cs)
| a == b = unify cs
| VarTy v <- a =
if occurs v b
then error (T.unpack ("Occurs check: " <> prettyType a <> " ~ " <>
prettyType b))
else let subbed = M.singleton v b
in do rest <- unify (substitute subbed cs)
return (rest <> subbed)
| VarTy v <- b =
if occurs v a
then error (T.unpack ("Occurs check: " <> prettyType a <> " ~ " <>
prettyType b))
else let subbed = M.singleton v a
in do rest <- unify (substitute subbed cs)
return (rest <> subbed)
| FunTy a1 b1 <- a
, FunTy a2 b2 <- b =
unify ([(a1,a2),(b1,b2)] <>
cs)
| QuotedTy a1 <- a
, QuotedTy b1 <- b =
unify ([(a1,b1)] <> cs)
| otherwise =
error (T.unpack ("Couldn't match expected type: " <> prettyType a <>
"\nagainst type: " <> prettyType b))
-- | Occurs check.
occurs :: Name Type -> Type -> Bool
occurs x (VarTy y)
| x == y = True
| otherwise = False
occurs x (FunTy a b) =
occurs x a ||
occurs x b
occurs x (QuotedTy t) = occurs x t
occurs _ UnitTy = False
occurs _ SymbolTy = False
-- | Substitute the unified type into the constraints.
substitute :: Map (Name Type) Type -> [(Type,Type)] -> [(Type,Type)]
substitute subs = map go
where go (a,b) = (replace subs a,replace subs b)
-- | Apply a substitution to a type.
replace :: Map (Name Type) Type -> Type -> Type
replace s' t' = M.foldrWithKey go t' s'
where go s1 t (VarTy s2)
| s1 == s2 = t
| otherwise = VarTy s2
go s t (FunTy t2 t3) =
FunTy (go s t t2)
(go s t t3)
go s t (QuotedTy qt) =
QuotedTy (go s t qt)
go _ _ UnitTy = UnitTy
go _ _ SymbolTy = SymbolTy
-- | Generate a new name for a type.
genSym :: MonadState (Stream (Name Type)) m => m (Name Type)
genSym = do Stream next stream <- get
put stream
return next
-- | An infinite stream of names.
nameStream :: Stream (Name Type)
nameStream = go 'b' (0 :: Integer)
where go c n =
Stream (Name (T.pack (c :
if n == 0
then ""
else show n)))
(go (toEnum (fromEnum 'a' + (mod (fromEnum c - fromEnum 'a' + 1) 26)))
(if c == 'z'
then n + 1
else n))
--------------------------------------------------------------------------------
-- Pretty printing
-- | Pretty printing for type.
prettyType :: Type -> Text
prettyType = go
where go t =
case t of
UnitTy -> "()"
SymbolTy -> "Symbol"
VarTy (Name n) -> n
FunTy a b -> (case a of
FunTy{} -> "(" <> go a <> ")"
_ -> go a)
<> " -> " <> go b
QuotedTy qt ->
"'" <>
case qt of
FunTy{} -> "(" <> go qt <> ")"
_ -> go qt
-- | Pretty printing for expression.
prettyExp :: Exp -> Text
prettyExp = go
where go t =
case t of
Unit -> "()"
Var (Name name) -> name
Fun (Name n) _ty e -> "(fn " <> n <> " " <> go e <> ")"
App f x -> "(" <> go f <> " " <> go x <> ")"
TypedQuote e -> go e
Quote e -> go e
Eval _ -> "eval"
--------------------------------------------------------------------------------
-- Instances
-- | Handy for debugging.
instance IsString (Name a) where
fromString = Name . fromString
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment