License	BSD-3-Clause
Safe Haskell	None
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 a where
- BApp :: forall a1 a. BTerm (a1 -> a) -> BTerm a1 -> BTerm a
- BConst :: forall a. Const a -> BTerm a
data OTerm (a :: [Type]) b where
- E :: forall b (a :: [Type]). BTerm b -> OTerm a b
- V :: forall b (g :: [Type]). OTerm (b ': g) b
- N :: forall (g :: [Type]) a1 b. OTerm g (a1 -> b) -> OTerm (a1 ': g) b
- W :: forall (g :: [Type]) b a1. OTerm g b -> OTerm (a1 ': g) b
bracket :: TTerm ('[] :: [Type]) a -> BTerm a
conv :: forall (g :: [Type]) a. TTerm g a -> OTerm g a

Documentation

data BTerm a where Source #

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

Constructors

BApp :: forall a1 a. BTerm (a1 -> a) -> BTerm a1 -> BTerm a
BConst :: forall a. 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 (a :: [Type]) b 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 :: forall b (a :: [Type]). BTerm b -> OTerm a b
V :: forall b (g :: [Type]). OTerm (b ': g) b
N :: forall (g :: [Type]) a1 b. OTerm g (a1 -> b) -> OTerm (a1 ': g) b
W :: forall (g :: [Type]) b a1. OTerm g b -> OTerm (a1 ': 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 ('[] :: [Type]) 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 :: forall (g :: [Type]) a. TTerm g a -> OTerm g a Source #

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