UTLC++/Generic

UTLC++.hs

-- see also previous gist https://gist.github.com/glaebhoerl/466267f0c977cef74202f167d6493cc0 and tweets https://twitter.com/glaebhoerl/status/1129851506067427329
-- here we accomplish the same thing but in a totally different way, by relying on the host language for basically everything

{-# LANGUAGE LambdaCase, GADTs, TypeOperators, DataKinds, PolyKinds, Strict, DeriveFunctor, RankNTypes, TypeFamilies, ConstraintKinds #-}

import Prelude hiding (product, sum)
import Data.Type.Equality
import GHC.Exts (Constraint)



--------------------------------------------------------------------------------------------------------------------------------------- utility

-- this thing shows up often: it's a constructive proof that the type-level list `list` contains the element `elem`, the proof being its index
data Index list elem where
    Head ::                    Index (elem  : list) elem
    Tail :: Index list elem -> Index (other : list) elem

-- this thing shows up often enough that it's included in the standard library :)
-- it's how we convince the typechecker that if two things are at the same index in a type-level list, then they must be equal
instance TestEquality (Index list) where
    testEquality = curry $ \case
        (Head,       Head)       -> Just Refl
        (Tail tail1, Tail tail2) -> testEquality tail1 tail2
        (_,          _)          -> Nothing



--------------------------------------------------------------------------------------------------------------------------------------- the actual thing

-- an introduction form is just "some data", here represented as a type containing instances of the eventual expression type
-- an untyped lambda calculus doesn't really have "types" so we use the word "constructor" for the different things it can have, like functions, pairs, etc.
-- constructors have *two* type arguments, both instantiated with the same expression type, for reasons
type Intro ctor expr = ctor expr expr

-- an elimination form is something which takes the corresponding introduction form and computes some result from it
-- any details of the elimination, e.g. which component of the pair to project, what argument to apply a function to, etc., can be "captured in the closure"
type Elim ctor expr = ctor expr expr -> expr

-- in the general case an expression is parameterized over a type-level list of what constructors it may consist of
-- meanwhile `meta` will only be needed so that we can actually inspect and print expressions -- you can safely ignore it for now
-- (notice that the Expr datatype, via `Elim` among others, contains plain Haskell functions (->) in it, which *very much* do not have a `Show` instance)
data Expr ctors meta where
    -- an expression may be either an introduction, or an elimination, of any constructor in the list, as witnessed by its `Index`

    -- we require that constructors be functors in their second argument, but not their first
    -- for instance, we want to be able to have functions `(->)` as one of the constructors
    Intro :: Functor (ctor (Expr ctors meta)) => Intro ctor (Expr ctors meta) -> Index ctors ctor -> Expr ctors meta

    -- an elimination stores both the subexpression to be eliminated, as well as the eliminator to do it with
    Elim  :: Expr ctors meta                  -> Elim  ctor (Expr ctors meta) -> Index ctors ctor -> Expr ctors meta

    -- "actual expressions" will have type `forall meta. Expr Ctors meta`, meaning this constructor may *not* occur in them
    -- it will be used to inject identifier strings into the expression "from outside" for pretty-printing purposes
    Meta  :: meta                                                                                 -> Expr ctors meta

-- the basic idea is that when we can't do a reduction directly, we fmap the elimination into the subterm
eval :: Expr ctors meta -> Expr ctors meta
eval = \case
    -- funnily enough, evaluation under binders (as well as all other data) can *also* be done using fmap, which I hadn't anticipated at the outset
    Intro intro i
        -> Intro (fmap eval intro) i

    -- if we have an elimination applied to another elimination, evaluate the inner one until a redex is exposed to the outer one
    Elim (subject@Elim{}) elim i
        -> eval (Elim (eval subject) elim i)

    -- a redex!
    Elim (Intro intro i2) elim i1
        | Just Refl <- testEquality i1 i2
            -- if both the introduction and elimination are of the same constructor, we can actually reduce
            -> elim intro
        | otherwise
            -- we fmap the elimination into the body of the introduction form, where it can hopefully meet another, matching intro
            -- this line is the *only* part which deals with these "nonstandard reduction rules"
            -- if you want to make like a normal language instead, you would simply report an error here
            -> Intro (fmap (\expr -> eval (Elim expr elim i1)) intro) i2

    -- since we are parametric over `meta`, we are obliged to just pass them through
    -- I think this is the analogue of a neutral form from a "normal" normalizer/evaluator
    Elim (Meta meta) elim i
        -> Elim (Meta meta) (eval . elim) i

    Meta meta
        -> Meta meta



--------------------------------------------------------------------------------------------------------------------------------------- language from the previous gist

-- we can use the type parameters of a constructor to control which positions eliminations "get fmapped into"
-- here we say "all positions"
data Both    x a = Both { fst' :: a,  snd' :: a } deriving Functor
data Either' x a = Left' a | Right' a             deriving Functor

type Ctors = [(->), Both, Either']

-- we could also use the standard Haskell pair and Either types, in which case they would be "biased", and fmap would only go into one position
-- or also things like: `data Neither a b = Left | Right`

type E = Expr Ctors

arrow :: Index Ctors (->)
arrow = Head

product :: Index Ctors Both
product = Tail Head

sum :: Index Ctors Either'
sum = Tail (Tail Head)

lam :: (E meta -> E meta) -> E meta
lam f = Intro f arrow

app :: E meta -> E meta -> E meta
app f a = Elim f (\f' -> f' a) arrow

both :: Both (E meta) (E meta) -> E meta
both p = Intro p product

split :: E meta -> (Both (E meta) (E meta) -> E meta) -> E meta
split p f = Elim p f product

first :: E meta -> E meta
first e = split e fst'

second :: E meta -> E meta
second e = split e snd'

inject :: Either' (E meta) (E meta) -> E meta
inject e = Intro e sum

left :: E meta -> E meta
left = inject . Left'

right :: E meta -> E meta
right = inject . Right'

match :: E meta -> (E meta -> E meta) -> (E meta -> E meta) -> E meta
match e f g = Elim e (\case Left' a -> f a; Right' b -> g b) sum

main :: IO ()
main = putStrLn (renderExpr example) >> putStrLn (renderExpr (eval example))

example :: forall meta. E meta
example = both (Both (lam $ \a -> a) (lam $ \a -> a)) `app` (lam $ \a -> lam $ \b -> a)



--------------------------------------------------------------------------------------------------------------------------------------- pretty-printing in general

renderExpr :: RenderCtors ctors => (forall a. Expr ctors a) -> String
renderExpr = render 'a'

-- we use Chars for variable names because they have a convenient `Enum` instance
class Render a where
    render :: Char -> a -> String

class RenderCtor ctor where
    renderIntro :: Render expr => Char -> (Char -> expr) ->         Intro ctor expr -> String
    renderElim  :: Render expr => Char -> (Char -> expr) -> expr -> Elim  ctor expr -> String

-- is there any way to do this without using TypeFamilies and ConstraintKinds to *compute* the necessary constraint?!
type family RenderCtors ctors :: Constraint where
    RenderCtors '[]          = ()
    RenderCtors (ctor:ctors) = (RenderCtor ctor, RenderCtors ctors)

instance (RenderCtors ctors, meta ~ Char {- eh -}) => Render (Expr ctors meta) where
    render c =
        let
            helper :: RenderCtors ctors => (RenderCtor ctor => result) -> Index ctors ctor -> result -- ugh
            helper f = \case
                Head      -> f
                Tail tail -> helper f tail
        in \case
            Intro     intro i -> helper (renderIntro c Meta      intro) i
            Elim expr elim  i -> helper (renderElim  c Meta expr elim)  i
            Meta c            -> [c]



--------------------------------------------------------------------------------------------------------------------------------------- pretty-printing in particular

instance RenderCtor (->) where
    renderIntro c meta f      = "\\" ++ [c] ++ " -> " ++ render (succ c) (f (meta c))
    renderElim  c meta e elim = render c e ++ " " ++ render c (elim id)

instance RenderCtor Both where
    renderIntro c meta (Both e1 e2) = "(" ++ render c e1 ++ ", " ++ render c e2 ++ ")"
    renderElim  c meta e elim       = "let (" ++ [c] ++ ", " ++ [succ c] ++ ") = " ++ render c e ++ " in " ++ render (succ (succ c)) (elim (Both (meta c) (meta (succ c))))

instance RenderCtor Either' where
    renderIntro c meta lr     = case lr of Left' e -> "Left " ++ render c e; Right' e -> "Right " ++ render c e
    renderElim  c meta e elim = "case " ++ render c e ++ " of Left " ++ [c] ++ " -> " ++ render (succ c) (elim (Left' (meta c))) ++ "; Right " ++ [c] ++ " -> " ++ render (succ c) (elim (Right' (meta c)))