AnIntro.md

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) ())) :: ()
()

Type.hs

{-# 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