Safe Haskell	Safe-Inferred
Language	Haskell2010

Syntax

Contents

Terms
Utilities

Description

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 :: *)
- = IntS Integer
- | FloatS Double
- | BoolS Bool
- | SymS Symbol
- | ListS [a]
data Cbpv (a :: *)
- = VoidA
- | IntA Integer
- | FloatA Double
- | BoolA Bool
- | SymA Symbol
- | OpA Symbol [a]
- | SuspendA a
- | ResumeA a
- | FunA [Symbol] a
- | AppA a [a]
- | LetA Symbol a a
- | LetrecA [(Symbol, a)] a
- | ResetA a
- | ShiftA Symbol a
- | IfA a a a
type CbpvExp = Cofree Cbpv ()
annotate :: (Monad m, Traversable f, Show a) => Free f a -> m (Cofree f ())
deps :: Map Symbol CbpvExp -> CbpvExp -> [Symbol]
isPositive :: Cbpv a -> Bool
opList :: [Symbol]
sexprToCbpv :: Cofree SExpr () -> Free Cbpv String
boolS :: Bool -> Free SExpr ()
intS :: Integer -> Free SExpr ()
floatS :: Double -> Free SExpr ()
symS :: Symbol -> Free SExpr ()
listS :: [Free SExpr a] -> Free SExpr a

Documentation

type Symbol = String Source #

Terms

data SExpr (a :: *) Source #

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.

Constructors

IntS Integer
FloatS Double
BoolS Bool
SymS Symbol
ListS [a]

Instances

Instances details

Foldable SExpr Source #
Instance details Defined in Syntax Methods 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 # toList :: SExpr a -> [a] # null :: SExpr a -> Bool # length :: SExpr a -> Int # elem :: Eq a => a -> SExpr a -> Bool # maximum :: Ord a => SExpr a -> a # minimum :: Ord a => SExpr a -> a # sum :: Num a => SExpr a -> a # product :: Num a => SExpr a -> a #
Traversable SExpr Source #
Instance details Defined in Syntax Methods traverse :: Applicative f => (a -> f b) -> SExpr a -> f (SExpr b) # sequenceA :: Applicative f => SExpr (f a) -> f (SExpr a) # mapM :: Monad m => (a -> m b) -> SExpr a -> m (SExpr b) # sequence :: Monad m => SExpr (m a) -> m (SExpr a) #
Functor SExpr Source #
Instance details Defined in Syntax Methods fmap :: (a -> b) -> SExpr a -> SExpr b # (<$) :: a -> SExpr b -> SExpr a #

data Cbpv (a :: *) 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.

Constructors

VoidA	1 / ⊥
IntA Integer	integer literal value
FloatA Double	floating point literal value
BoolA Bool	boolean literal value
SymA Symbol	identifier symbol
OpA Symbol [a]	application of an 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

Instances details

Foldable Cbpv Source #
Instance details Defined in Syntax Methods 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 # toList :: Cbpv a -> [a] # null :: Cbpv a -> Bool # length :: Cbpv a -> Int # elem :: Eq a => a -> Cbpv a -> Bool # maximum :: Ord a => Cbpv a -> a # minimum :: Ord a => Cbpv a -> a # sum :: Num a => Cbpv a -> a # product :: Num a => Cbpv a -> a #
Eq1 Cbpv Source #
Instance details Defined in Syntax Methods liftEq :: (a -> b -> Bool) -> Cbpv a -> Cbpv b -> Bool #
Ord1 Cbpv Source #
Instance details Defined in Syntax Methods liftCompare :: (a -> b -> Ordering) -> Cbpv a -> Cbpv b -> Ordering #
Show1 Cbpv Source #
Instance details Defined in Syntax Methods liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Cbpv a -> ShowS # liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Cbpv a] -> ShowS #
Traversable Cbpv Source #
Instance details Defined in Syntax Methods traverse :: Applicative f => (a -> f b) -> Cbpv a -> f (Cbpv b) # sequenceA :: Applicative f => Cbpv (f a) -> f (Cbpv a) # mapM :: Monad m => (a -> m b) -> Cbpv a -> m (Cbpv b) # sequence :: Monad m => Cbpv (m a) -> m (Cbpv a) #
Functor Cbpv Source #
Instance details Defined in Syntax Methods fmap :: (a -> b) -> Cbpv a -> Cbpv b # (<$) :: a -> Cbpv b -> Cbpv a #
Eq a => Eq (Cbpv a) Source #
Instance details Defined in Syntax Methods (==) :: Cbpv a -> Cbpv a -> Bool # (/=) :: Cbpv a -> Cbpv a -> Bool #

type CbpvExp = Cofree Cbpv () Source #

The primary form of our intermediate language.

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.

deps :: Map Symbol CbpvExp -> CbpvExp -> [Symbol] Source #

isPositive :: Cbpv a -> Bool Source #

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

opList :: [Symbol] Source #

UNSTABLE Canonical list of built-in operators.

sexprToCbpv :: Cofree SExpr () -> Free Cbpv String Source #

Builds a Cbpv expression from an SExpr syntax tree.

boolS :: Bool -> Free SExpr () Source #

intS :: Integer -> Free SExpr () Source #

floatS :: Double -> Free SExpr () Source #

symS :: Symbol -> Free SExpr () Source #

listS :: [Free SExpr a] -> Free SExpr a Source #