Safe Haskell | None |
---|---|

Language | Haskell2010 |

## The theory

Call-By-Push-Value is the intermediate language we are using here because

- it subsumes both call-by-value and call-by-name, and
- the type system for it is really something.

CBPV is able to subsume both CBV and CBN evaluation strategies because the type
system can enforce at compile-time that all function arguments are so-called
*positive* terms: fully-evaluated, static, terminated *data*.

These are contrasted with *negative* terms, which are computations (if you want
to be really precise, they represent transitions of the evaluator virtual
machine).

There is so much more to say here. Stay tuned!

## The implementation

The Parser module generates `SExpr`

values, after which you may convert from
`sexpr_to_cbpv`

.

The grammars are defined as non-recursive, higher-order types; where they would
reference themselves they instead reference their type parameter.
When "fixed" with the `Free`

monad type, the resulting new type defines a number
of convenient smart constructors for building syntax trees (say, in a `Parser`

).

And when fixed with the `Cofree`

comonad type the resulting type defines a new
grammar pairing every "branch" in the tree with some annotation value.

Both of these are very convenient, and what's more, the conversion from the
former to the latter in `annotate`

is quite elegant, I think.

## Synopsis

- type Symbol = String
- data SExpr (a :: *)
- data Cbpv (a :: *)
- type CbpvExp = Cofree Cbpv ()
- annotate :: (Monad m, Traversable f, Show a) => Free f a -> m (Cofree f ())
- deps :: Map Symbol CbpvExp -> CbpvExp -> [Symbol]
- is_positive :: Cbpv a -> Bool
- prim_list :: [Symbol]
- sexpr_to_cbpv :: Show a => Free SExpr a -> Free Cbpv String

# Documentation

# Terms

A very simple s-expression language. An s-expression is either some atom (symbol, number, boolean) or a white-space-delimited list of s-expressions surrounded by parentheses. For now, any surface syntax (ie, stuff a human such as yours truly would be expected to type) will be based on s-expressions, and be able to make use of the same s-expression parser defined in a sibling module. Conversion to more structured intermediate forms is taken care of by other functions.

#### Instances

Functor SExpr Source # | |

Foldable SExpr Source # | |

Defined in Syntax fold :: Monoid m => SExpr m -> m # foldMap :: Monoid m => (a -> m) -> SExpr a -> m # foldMap' :: Monoid m => (a -> m) -> SExpr a -> m # foldr :: (a -> b -> b) -> b -> SExpr a -> b # foldr' :: (a -> b -> b) -> b -> SExpr a -> b # foldl :: (b -> a -> b) -> b -> SExpr a -> b # foldl' :: (b -> a -> b) -> b -> SExpr a -> b # foldr1 :: (a -> a -> a) -> SExpr a -> a # foldl1 :: (a -> a -> a) -> SExpr a -> a # elem :: Eq a => a -> SExpr a -> Bool # maximum :: Ord a => SExpr a -> a # minimum :: Ord a => SExpr a -> a # | |

Traversable SExpr Source # | |

Call-By-Push-Value
Call-By-Push-Value is a type system which polarizes terms and types into
*positive* and *negative* kinds.
Positive terms are literal values or data; they are "at rest"; "static".
Negative terms are functions; "in action"; "dynamic".
In doing so the type system is able to enforce evaluation order at compile
time.
`Cbpv`

is a meta-language chosen because of what can be built on top of it
and not because it is particularly pleasant on its own.

VoidA | 1 / ⊥ |

IntA Integer | integer literal value |

FloatA Double | floating point literal value |

BoolA Bool | boolean literal value |

SymA Symbol | identifier symbol |

PrimA Symbol [a] | application of a primitive operator to positive terms |

SuspendA a | negative -> positive negative terms (computations) |

ResumeA a | positive -> negative |

FunA [Symbol] a | pops and binds values from call stack, evals body |

AppA a [a] | pushes values onto call stack, evals operator |

LetA Symbol a a | evals first computation, binds its value in second |

LetrecA [(Symbol, a)] a | mutually recursive bindings |

ResetA a | delimits a continuation capture |

ShiftA Symbol a | captures and binds a continuation in a computation |

IfA a a a | first arg must be positive (boolean), others negative |

#### Instances

Functor Cbpv Source # | |

Foldable Cbpv Source # | |

Defined in Syntax fold :: Monoid m => Cbpv m -> m # foldMap :: Monoid m => (a -> m) -> Cbpv a -> m # foldMap' :: Monoid m => (a -> m) -> Cbpv a -> m # foldr :: (a -> b -> b) -> b -> Cbpv a -> b # foldr' :: (a -> b -> b) -> b -> Cbpv a -> b # foldl :: (b -> a -> b) -> b -> Cbpv a -> b # foldl' :: (b -> a -> b) -> b -> Cbpv a -> b # foldr1 :: (a -> a -> a) -> Cbpv a -> a # foldl1 :: (a -> a -> a) -> Cbpv a -> a # elem :: Eq a => a -> Cbpv a -> Bool # maximum :: Ord a => Cbpv a -> a # | |

Traversable Cbpv Source # | |

Eq1 Cbpv Source # | |

Ord1 Cbpv Source # | |

Show1 Cbpv Source # | |

Eq a => Eq (Cbpv a) Source # | |

# Utilities

annotate :: (Monad m, Traversable f, Show a) => Free f a -> m (Cofree f ()) Source #

This function converts a free monad representation of a language into one which annotates each expression with arbitrary metadata. One example use-case is annotating expressions with type information.

is_positive :: Cbpv a -> Bool Source #

Helper function answering the question: is this 'Free Cbpv a' expression atomic?