Skip to content

Instantly share code, notes, and snippets.

@chrisdone

chrisdone/AnIntro.md

Last active October 11, 2025 13:03
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save chrisdone/516489f4f27846712225 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save chrisdone/516489f4f27846712225 to your computer and use it in GitHub Desktop.
Download ZIP
Statically Typed Lisp
Raw
AnIntro.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.

--

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) ())) :: ()
()
Raw
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
@Blaisorblade
Copy link
Copy Markdown

Blaisorblade commented Dec 12, 2014

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).

@kmarekspartz
Copy link
Copy Markdown

kmarekspartz commented Dec 18, 2014

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!

@Gozala
Copy link
Copy Markdown

Gozala commented May 30, 2017

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment