type ::= expr
expr ::= varid
expr ::= expr expr
Example: x + y
is the same as (+) x y.
Functions
Function expressions are written as lambda expressions. The bound
variable must be given a type.
expr ::= \ (varid :: type) -> expr
Example: \ (x::Int) -> x+1
\ (a :: #) -> \ (x :: a) -> x
Function type
The function type is written much like a lambda expression, but there
is no leading \. Since Cayenne has dependent types the function type
binds a variable (of the argument type) that may occur in the result type.
expr ::= (varid :: type) -> type
Example: (x::Int) -> F x
expr ::= type -> type
expr ::= #
expr ::= data condef | ...
condef ::= conid type ...
conid ::= varid
Example: data C1 | C2 Int | C3 Int Bool
This is a data type, call it T, with three constructors, C1 of
type T, C2 of type Int->T, and
C3 of type Int->Bool->T.
To make recursive types you need a recursive definition, which is introduced below.
Note that a data type does not intruduce any new bound variables. The
constructors of a data type have no special status.
Constructors
To use a constructor of a data type you need to give both the name of
the constructor and the type that it belongs to.
expr ::= conid @ type
Example: True@(data False|True)
This is the second constructor in the type data False|True.
Example: C2@(data C1 | C2 Int | C3 Int Bool)
This is second constructor and the expression has type
Int->(data C1 | C2 Int | C3 Int Bool).
The type can in many cases be written as _ if the type
if the constructors is obvious from the context.
Example: C2@_
Case
Case expressions are used to scrutinize expressions of product type.
It has the following form:
expr ::= case expr of { casearm ; ... }
casearm ::= (conid) -> expr
In a case expression there is no need to give the type of the
constructors in the patterns.
Example: case x of { (True) -> False; (False) -> True; }
case y of {
(C1) -> 0;
(C2) -> \(x::Int) -> x;
(C3) -> \(y::Int) -> \(b::Bool) -> y;
}
Example:
case y of {
(C1) -> 0;
(C2 x) -> x;
(C3 y b) -> y;
}
Note how all constructor patterns are in parenthesis; this is to have
a syntactic way of distinguishing constructor patterns and variable patterns.
Record formation
Records are unordered labelled products. Record values are formed
according to the rule
expr ::= struct { [modifier] defn ; ... }
defn ::= labelid :: type = expr
labelid ::= varid
A record can contain an arbitrary number of components. Each
component has a label, a type, and a value. The label identifiers are
bound within the record construction, but unbound outside it. The
bindings are mutually recursive.
There is a lot of syntactic suger for the definitions in records.
Note that the word struct can be omitted when the layout rule is not used.
modifier ::= abstract | concrete | public | private
Example:
struct { x :: Int = 5; y :: Int = 4; }
struct { idInt :: Int->Int = \ (x::Int) -> x; two :: Int = idInt 2; }
struct { private x :: Int = 2+5; x2 :: Int = x*x; }
struct { concrete c :: Int = 2; inc :: Int->Int = \(x::Int)->x+1; }
Example: concrete struct { x::Int=5; y::Int=7; }
Record selection
Record selection is written with an infix `.' between an
expression and a label.
expr ::= expr . labelid
Example: r.x
Record types (products)
The notation for a record type is similar to that of the record
formation. The only difference is that for abstract components the
expression part is left out and there are no modifiers.
expr ::= sig { varid :: type [ = expr ] ; ... }
Note that the word sig can be omitted when the layout rule is not used.
Example (the types of the records above):
sig { x :: Int; y :: Int; }
sig { idInt :: Int->Int; two :: Int; }
sig { x2 :: Int; }
sig { c :: Int = 2; inc :: Int->Int; }
A peculiarity of the record type is that does not only contain type of each
component, but sometimes also its value!
This is mostly used to make the constructors of a data type known from
just the signature of a module (=record).
Having the value of a component in the type complicates testing types
for equality, but not in any essential way since arbitrary expression
need to be compared anyway with dependent types.
let expressions
Cayenne provides Haskell style let expressions to make
local bindings.
expr ::= let defn; ... in expr
The expression
let d1; d2; ... in e
is (semantically) equivalent to
struct { d1; d2; ...; r::t = e; }.r
where r is a fresh identifier and t is the
type of e.
open expressions
The open expression provides a convenient way to get
access to many components of a record.
expr ::= open expr use varid :: type [ =
varid ], ... in expr
The expression
open e use i1::t1=i1', i2::t2=i2', ... in e'
is (semantically) equivalent to
let i1::t1 = e.i1'; i2::t2 = e.i2'; ... in e'
If the second varid is left out it is assumed to be the same as
the first. The types can be omitted. So you normally write just
open e use i1, i2, ... in e'
expr ::= do expr { bind ; ... }
bind ::= varid :: type <- expr | expr
do expr { binds }
--->
open expr use (>>=), (>>), return in T { binds }
T { expr } ---> expr
T { expr ; binds } ---> expr >> T { binds }
T { arg <- expr ; binds } ---> expr
>>= \ arg -> T { binds }
Example:
do System$IO.Monad {
s :: String <- readFile "foo";
writeFile "bar" s;
}
struct {
Bool :: # = data False | True;
True :: Bool = True@Bool;
False :: Bool = False@Bool;
not :: Bool -> Bool = \ (x::Bool) ->
case x of {
(False) -> True;
(True) -> False;
};
}
Natural numbers:
struct {
Nat :: # = data Zero | Succ Nat;
add :: Nat -> Nat -> Nat = \ (x::Nat) -> \ (y::Nat) ->
case x of {
(Zero) -> y;
(Succ n) -> Succ (add n y);
};
}
expr ::= [ expr ]
expr ::= expr { eqstep ... }
eqstep ::= ={ DEF }= expr
eqstep ::= ={ expr }= expr