Swarm.Game.World.Abstract

Explicitly type-preserving bracket abstraction, a la Oleg Kiselyov. Turn elaborated, type-indexed terms into variableless, type-indexed terms with only constants and application.

For more information, see:

https://byorgey.wordpress.com/2023/07/13/compiling-to-intrinsically-typed-combinators/

Documentation

data BTerm :: Type -> Type where

Closed, fully abstracted terms. All computation is represented by combinators. This is the ultimate target for the bracket abstraction operation.

Constructors

BApp :: BTerm (a -> b) -> BTerm a -> BTerm b

BConst :: Const a -> BTerm a

Instances

Applicable BTerm

Defined in Swarm.Game.World.Abstract

Methods

($$) :: BTerm (a -> b) -> BTerm a -> BTerm b

HasConst BTerm

Defined in Swarm.Game.World.Abstract

Methods

embed :: Const a -> BTerm a

Show (BTerm t)

Defined in Swarm.Game.World.Abstract

Methods

showsPrec :: Int -> BTerm t -> ShowS

show :: BTerm t -> String

showList :: [BTerm t] -> ShowS

data OTerm :: [Type] -> Type -> Type where

These explicitly open terms are an intermediate stage in the bracket abstraction algorithm, i.e. they represent terms which have been only partially abstracted.

Constructors

E :: BTerm a -> OTerm g a

V :: OTerm (a ': g) a

N :: OTerm g (a -> b) -> OTerm (a ': g) b

W :: OTerm g b -> OTerm (a ': g) b

Instances

Applicable (OTerm g)

Defined in Swarm.Game.World.Abstract

Methods

($$) :: OTerm g (a -> b) -> OTerm g a -> OTerm g b

HasConst (OTerm g)

Defined in Swarm.Game.World.Abstract

Methods

embed :: Const a -> OTerm g a

bracket :: TTerm '[] a -> BTerm a

Bracket abstraction: convert the TTerm to an OTerm, then project out the embedded BTerm. GHC can see this is total since E is the only constructor that can produce an OTerm with an empty environment.

conv :: TTerm g a -> OTerm g a

Type-preserving conversion from TTerm to OTerm (conv + the Applicable instance). Taken directly from Kiselyov.