License	BSD-3-Clause
Safe Haskell	Safe-Inferred
Language	Haskell2010

Swarm.Game.World.Abstract

Description

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/

Synopsis

data BTerm :: Type -> Type where
- BApp :: BTerm (a -> b) -> BTerm a -> BTerm b
- BConst :: Const a -> BTerm a
data OTerm :: [Type] -> Type -> Type where
- 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
bracket :: TTerm '[] a -> BTerm a
conv :: TTerm g a -> OTerm g a

Documentation

data BTerm :: Type -> Type where Source #

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

Instances details

Applicable BTerm Source #
Instance details Defined in Swarm.Game.World.Abstract Methods ($$) :: BTerm (a -> b) -> BTerm a -> BTerm b Source #
HasConst BTerm Source #
Instance details Defined in Swarm.Game.World.Abstract Methods embed :: Const a -> BTerm a Source #
Show (BTerm t) Source #
Instance details 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 Source #

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

Instances details

Applicable (OTerm g) Source #
Instance details Defined in Swarm.Game.World.Abstract Methods ($$) :: OTerm g (a -> b) -> OTerm g a -> OTerm g b Source #
HasConst (OTerm g) Source #
Instance details Defined in Swarm.Game.World.Abstract Methods embed :: Const a -> OTerm g a Source #

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

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 Source #

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