Statically Typed Lisp

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

BCommentary.md

Note: I noticed this was posted to /r/programming but it's far from complete, it doesn't even have numbers or let/if/case special operators. It was just a Friday evening's whim to research whether quotation can be practically statically typed and what that might feel like. I'll have to implement at least case and let in order to deconstruct the quoted expressions and implement eval similar to Roots of Lisp before I can answer that to my satisfaction.

Including the reply I wrote in that thread:

As the author of this gist, static typing in general isn't the goal. There are a bunch of statically typed Lisps.

Shen has the type symbol for quoted things:

• '+ : symbol

My lisp has two types of quotation:

• '+ :: 'Symbol
• ~+ :: '(Int -> Int -> Int)

I'm not quite decided whether I want staged lambda-calculus, or this mixing style. What you end up with is a kind of non-opaque lambda:

• (lambda (x) (+ x x)) — this is opaque, you can't "look inside" this lambda. But it means the things inside can be statically typed.
• '(lambda (x) (+ x x)) — this is transparent, you can look inside the lambda. It's just a tree. It's not typed, the whole thing is just "symbol" or "tree of symbols".
• ~(lambda (x) (+ x x)) — this is both transparent and statically typed. The + must exist, which it does, and have a type, which it does, Int -> Int -> Int, therefore the type of the xs must be Int. So the whole expression has type: '(Int -> Int). Note the ', meaning "a quoted thing of type X".

So ~ ends up sitting somewhere in between a lambda and a quote.

I should be able to write:

(defmacro when (p body)
  ~(if ,p
       ,body
       ()))

And then the macro when will have type: 'Bool -> '() -> '(), if that makes sense. I cannot write, for example, (when 123 "go!"). This would be rejected before the macro is even expanded. A well-typed macro is interesting. Haskell doesn't have normal Lisp symbolic quotation, you can't just write 'foo, therefore I don't consider Haskell or its ML ancestors to be part of the Lisps family. It does have 'foo, it instead requires that foo exists as a name in scope. But it doesn't encode any type information, which is not very Haskelly either.

There's also the tricky problem of eval. In regular Lisp, eval throws exceptions. In even Shen this is true, because its quotation is not type-safe. Whereas if your eval is like in my little Lisp:

eval :: 'a -> a

Then the quoted symbol carries the type information and means that eval will at least never produce a type error.

Whether this works in practice I've yet to determine/decide. It's just an idea that interested me.

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

That's a very hard problem you're tackling here. Lisps can usually write self-interpreters, but typed self-interpreters are very hard (the usual conjecture is they don't exist for usual type systems, as a consequence of Gödel's theorems).* Providing eval as a builtin is one of the ways out, but then it's less clear that you can achieve other metaprogramming tasks — writing eval in the language is a kind of benchmark for its metaprogramming power.

*Should you want to read academic papers on how to do it, see papers at PLDI '09 (https://www.uni-marburg.de/fb12/ps/research/tsr?set_language=en) and POPL '15 ("Self-Representation in Girard's System U", not yet publicly available).

What is the distinction between typed quotation and lazy lambdas? I've been wondering how to describe exactly what macros provide relative to lazy lambdas (just syntactic flexibility, or something more?). This seems bring them closer.

Neat!

@chrisdone have you explored this beyond what's in the commentary ? Or have by a chance drawn some conclusions since ?