This is a brief guide to the terminology and syntax used in the monad-embed programming language. See the other documentation for a description of the semantics.
In monad-embed, every expression has a type, of kind *, and a flavor, which is a monad of kind * -> *.
As in Haskell, * is the kind of types and a -> b is the kind of type constructors. Also as in Haskell, types begin with capital letters and type variables begin with lower-case letters.
Unlike Haskell, monad-embed does not have syntactic sugar for applications of list or tuple constructors.
Function types are written in one of the following two forms:
a -> {f} r[{f'} a] -> {f} ra is the argument type, r is the return type, and f is the flavor of the function's return value. The second form is the type of a lazy function. Note that in a lazy function, f' specifies the flavor of the lazy function's argument.
The type IO indicates the IO monad. The type t / m indicates the monad constructed by composing the monad transformer t with the monad m.
Algebraic data types work approximately like they do in Haskell. For example, here's the definition of the List type constructor:
data List (a :: *) = {
Nil;
Cons a (List a);
};
Because monad-embed lacks kind inference, you must specify the kind of each type variable explicitly.
By default, fields are strict. To make a field lazy, use the syntax [{f} t], where f is the flavor of the lazy field and t is its type. For example, here is the definition of a lazy list, ZList:
data ZList (f :: * -> *) (a :: *) = {
ZNil;
ZCons a [{f} ZList a];
};
The form of a type signature is as follows. Don't forget the semicolon.
name :: (var :: kind, ...) => {flavor} type;
Monad-embed lacks kind inference, so the kinds of any polymorphic variables must be specified manually.
In a type signature, the flavor of a function can be omitted, and it will be assumed to be the same as that of the definition.
Here are some examples of type signatures. Note that these are just type signatures; these do not actually define id, map, and zcat.
-- Strict function returning the same type as its argument. Note that
-- "{f}" modifies the entire function type "a -> a", not just the
-- first "a".
id :: (a :: *, f :: * -> *) => {f} a -> a;
-- Takes a function and a list. Again, {f} modifies the entire type
-- "(a -> b) -> List a -> List b"
map :: (f :: * -> *, a :: *, b :: *) => {f} (a -> b) -> List a -> List b;
-- Takes two ZLists, the second of which is passed lazily to zcat
zcat :: (f :: * -> *, a :: *) => {f} ZList f a -> [ZList f a] -> ZList f a;
Definitions are of the form "name = value;". Note the semicolon. There is no support for function-style definitions of the form "name a1 a2 ... = value;" as in Haskell.
Lambda-expressions are of the form (\ arg -> body), for a strict function, or (\ [arg] -> body), for a lazy function. Strict function application is (function arg); lazy function application is (function [arg]). The expression (a `f` b) is syntactic sugar for (f a b). Other than that, there are no infix operators.
Numeric literals can be integers (555) or fractional (3.14159). You can use prefix negation "-" with numeric literals, but not in any other context. Use the function negate to negate something that is not a numeric literal. Numeric literals have type Number. String literals are delimited by double quotes, such as "Hello world!\n". String literals have type String. Strings are not lists; there is no character type.
Constructor application is as in Haskell. Pattern matching is done using the case statement: case x of { a -> b; c -> d; }. Note the semicolons. Patterns can be single variables, constructors, or a wildcard "_" to match anything. Remember to use brackets [] when matching a lazy constructor field.
For example, we can define a Bool type and boolean not as follows:
data Bool = { True; False; };
not :: (f :: * -> *) => {f} Bool -> Bool;
not = \ x -> case x of {
True -> False;
False -> True;
};
For a slightly more complicated example, we can define a function to concatenate two lazy lists as follows:
zcat = \ a [b] -> case a of {
ZNil -> b;
ZCons x [xs] -> ZCons x [zcat xs [b]];
};
The do keyword can be used for local variable bindings, like Haskell's let and for sequencing actions, like Haskell's do. A do-expression looks like this:
do {
var = value; -- Strict variable binding
var2 =[] value2; -- Lazy variable binding
value3; -- Evaluates value3 without binding it to anything
} then x; -- The entire do-block takes on the value of x
Local variable bindings are monomorphic and cannot refer to themselves or to local variable bindings that come after them. Recursive or polymorphic values are only legal at the top level.
wrap and unwrap are actually functions, defined as compiler builtins. Their types are:
wrap :: (t :: (* -> *) -> * -> *, m :: * -> *, a :: *)
=> {t / m}
[{m} t m a] -> {t / m} a;
unwrap :: (t :: (* -> *) -> * -> *, m :: * -> *, a :: *)
=> {m}
[{t / m} a] -> {m} t m a;