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.

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.

--

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