Skip to content

Instantly share code, notes, and snippets.

@joom
Last active February 27, 2019 13:19
Show Gist options
  • Save joom/81c328421ded6372ceffdcbbf58552e5 to your computer and use it in GitHub Desktop.
Save joom/81c328421ded6372ceffdcbbf58552e5 to your computer and use it in GitHub Desktop.
Automatically going back and forth between a Haskell value and its Scott encoding, using Data and Typeable. For more explanation, look for my work on "Direct Reflection for Free!"
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE IncoherentInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UndecidableInstances #-}
module Scott where
import qualified Data.Map as M
import Data.Maybe
import Control.Monad.State.Strict
import Text.Parsec.String
import Text.Parsec
import Unsafe.Coerce
import Data.Typeable
import Data.Data
-- Lambda calculus
data Exp =
Var String -- x
| App Exp Exp -- e1 e2
| Abs String Exp -- \x.x or λx.x, also works with nested \x y.x and such
| StrLit String -- "asdf", can escape "as\"df"
| IntLit Int -- 0
| MkUnit -- ()
| Quasiquote Exp -- `(e), where e is any expression
| Antiquote Exp -- ~(e), where e is an AST Scott encoding
| Parse Exp -- {e}, where e is a string expression, returns AST
| Pretty Exp -- [e], where e is an AST Scott encoding, returns a string
deriving (Show, Eq, Ord, Data, Typeable)
parseExp :: String -> Either ParseError Exp
parseExp input = parse exp "λ−calculus" input
where
lexeme p = spaces *> p <* spaces
parens p = char '(' *> p <* char ')'
quote p = string "`(" *> (Quasiquote <$> p) <* char ')'
antiquote p = string "~(" *> (Antiquote <$> p) <* char ')'
parseBr p = char '{' *> (Parse <$> p) <* char '}'
prettyBr p = char '[' *> (Pretty <$> p) <* char ']'
name = (:) <$> letter <*> many (digit <|> letter)
parseAbs = do
(char '\\' <|> char 'λ')
vs <- many1 (lexeme name)
lexeme $ char '.'
body <- exp
return $ foldr Abs body vs
parseVar = Var <$> name
parseUnit = string "()" *> return MkUnit
escape = do
d <- char '\\'
c <- oneOf "\\\"0nrvtbf" -- all the characters which can be escaped
return [d, c]
nonEscape = noneOf "\\\"\0\n\r\v\t\b\f"
character = fmap return nonEscape <|> escape
parseString = char '"' *> (StrLit . concat <$> many character) <* char '"'
parseInt = IntLit . read <$> many1 (digit :: Parser Char)
nonApp = try parseUnit <|> parens exp
<|> parseString <|> parseInt
<|> quote exp <|> antiquote exp <|> parseBr exp <|> prettyBr exp
<|> parseAbs <|> parseVar
exp = chainl1 (lexeme nonApp) $ return App
pretty :: Exp -> String
pretty (Var s) = s
pretty e@(App _ _) = "(" ++ go e ++ ")"
where go (App e1 e2) = go e1 ++ " " ++ pretty e2
go e = pretty e
pretty e@(Abs _ _) = "(λ" ++ go e ++ ")"
where go (Abs x e) = " " ++ x ++ go e
go e = ". " ++ pretty e
pretty (StrLit s) = "\"" ++ s ++ "\""
pretty (IntLit i) = show i
pretty MkUnit = "()"
pretty (Quasiquote e) = "`(" ++ pretty e ++ ")"
pretty (Antiquote e) = "~(" ++ pretty e ++ ")"
pretty (Parse e) = "{" ++ pretty e ++ "}"
pretty (Pretty e) = "[" ++ pretty e ++ "]"
lams :: [String] -> Exp -> Exp
lams xs e = foldr Abs e xs
apps :: [Exp] -> Exp
apps = foldl1 App
eval' :: M.Map String Exp -> Exp -> Exp
eval' env e@(Var x) = fromMaybe e (M.lookup x env)
eval' env (App (Abs x body) e) = eval' (M.insert x (eval' env e) env) body
eval' env (App e1 e2)
| eval' env e1 == e1 && eval' env e2 == e2 = App e1 e2
| otherwise = eval' env (App (eval' env e1) (eval' env e2))
eval' env (Abs x body) = Abs x $ eval' (M.insert x (Var x) env) body
eval' env (Quasiquote e) = reflect e
eval' env (Antiquote e) = fromJust (reify (eval e))
eval' env (Parse e) = let StrLit s = eval e in
case parseExp s of
Left err -> error $ show err
Right e' -> reflect e'
eval' env (Pretty e) = StrLit $ pretty e
eval' env e = e
eval :: Exp -> Exp
eval = eval' M.empty
-- Generic programming
getTypeRep :: forall a. Typeable a => TypeRep
getTypeRep = typeOf @a undefined
getDataType :: forall a. Data a => DataType
getDataType = dataTypeOf @a undefined
getConstrs :: forall a. Data a => Maybe [Constr]
getConstrs = case dataTypeRep (getDataType @a) of
AlgRep cs -> Just cs
_ -> Nothing
getNumOfConstrs :: forall a. Data a => Int
getNumOfConstrs = maybe 0 id (length <$> getConstrs @a)
constrToScott :: forall a. Data a => Constr -> ([String], String)
constrToScott c = (ctorArgs, ctorArgs !! (constrIndex c - 1))
where
names s = map ((s ++) . show) [0..]
ctorArgs = take (getNumOfConstrs @a) (names "c")
-- ^ arg names representing each ctor
collectAbs :: Exp -> ([String], Exp)
collectAbs (Abs x e) = let (l, e') = collectAbs e in (x:l, e')
collectAbs e = ([], e)
spineView :: Exp -> (Exp, [Exp])
spineView (App e1 e2) = let (f, l) = spineView e1 in (f, l ++ [e2])
spineView e = (e, [])
-- The interesting type class
class Bridge a where
reflect :: a -> Exp
reify :: Exp -> Maybe a
instance Bridge String where
reflect s = StrLit s
reify (StrLit s) = Just s
reify _ = Nothing
instance Bridge Int where
reflect n = IntLit n
reify (IntLit n) = Just n
reify _ = Nothing
instance Data a => Bridge a where
reflect v
| getTypeRep @a == getTypeRep @Int = reflect @Int (unsafeCoerce v)
| getTypeRep @a == getTypeRep @String = reflect @String (unsafeCoerce v)
| otherwise =
lams args (apps (Var c : gmapQ reflectArg v))
where
(args, c) = constrToScott @a (toConstr v)
reflectArg :: forall d. Data d => d -> Exp
reflectArg x = reflect @d x
reify e
| getTypeRep @a == getTypeRep @Int = unsafeCoerce (reify @Int e)
| getTypeRep @a == getTypeRep @String = unsafeCoerce <$> (reify @String e)
| otherwise =
case collectAbs e of -- dissect the nested lambdas
([], _) -> Nothing
(args, body) ->
case spineView body of -- dissect the nested application
(Var c, rest) -> do
ctors <- getConstrs @a
ctor <- lookup c (zip args ctors)
evalStateT (fromConstrM reifyArg ctor) rest
_ -> Nothing
where
reifyArg :: forall d. Data d => StateT [Exp] Maybe d
reifyArg = do e <- gets head
modify tail
lift (reify @d e)
-- | Very rudimentary REPL, ideally we'd like to use repline or haskeline
-- but I wanted to make the module self-contained.
main :: IO ()
main = do
putStr ">> "
x <- getLine
case parseExp x of
Left err -> putStr "ERROR: " >> print err
Right exp -> putStrLn (pretty $ eval exp)
main
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment