psilo
Safe HaskellNone
LanguageHaskell2010

Syntax

Description

The theory

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

  1. it subsumes both call-by-value and call-by-name, and
  2. 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

Documentation

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.

Instances

Instances details
Functor SExpr Source # 
Instance details

Defined in Syntax

Methods

fmap :: (a -> b) -> SExpr a -> SExpr b #

(<$) :: a -> SExpr b -> SExpr a #

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

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
Functor Cbpv Source # 
Instance details

Defined in Syntax

Methods

fmap :: (a -> b) -> Cbpv a -> Cbpv b #

(<$) :: a -> Cbpv b -> Cbpv a #

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 #

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

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 #

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.

is_positive :: Cbpv a -> Bool Source #

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

op_list :: [Symbol] Source #

UNSTABLE Canonical list of built-in operators.

sexpr_to_cbpv :: Show a => Free SExpr a -> Free Cbpv String Source #

VALIDATE and convert S-expressions to an CBPV intermediate representation. The base type is used for error-reporting; here, we simply report errors as Strings.