#{
    Notes on an ML-like programming language
    Kevin Watkins
    March 2005

    The language (even with lazy extensions) is CBV.
    Lowercase variables always stand for values.
    Uppercase (proper) names stand for expressions, and
      can be recursive (i.e. they're elaborated into let name ...).
#}

### Syntax of definitions

# curried style A
1st a b is a;
1st x y == x;
2nd a b is b;
2nd x y == y;

# curried style B
# -> introduces an anonymous function
# => is the type of an anonymous function
1st is fn a b => a;
1st == fn x y -> x;
2nd is fn a b => b;
2nd == fn x y -> y;

# curried style C
# if "fn" takes exactly one argument it can be dropped
1st is a => b => a;
1st == x -> y -> x;
2nd is a => b => b;
2nd == x -> y -> y;

# uncurried style A
Swap (a, b) is (b, a);
Swap (x, y) == (y, x);
# fewer parens
# , has higher precedence than -> == but lower than everything else
Swap (a, b) is b, a;
Swap (x, y) == y, x;
# This would be bogus
#   Swap x, y == y, x
# because it would mean
#   (Swap x), y == y, x

# uncurried style B
Swap is fn (a, b) => (b, a);
Swap == fn (x, y) -> (y, x);
# fewer parens
Swap is fn (a, b) => b, a;
Swap == fn (x, y) -> y, x;

# uncurried style C
Swap is (a, b) => (b, a);
Swap == (x, y) -> (y, x);
# fewer parens
Swap is a, b => b, a;
Swap == x, y -> y, x;

# matching style A
Snoc (List a)    a is List a;
Snoc Nil         y == Cons y Nil;
Snoc (Cons x xs) y == Cons x (Snoc xs y);

# matching style B
# (braces introduce an anonymous function with multiple
# cases; if there's only one case the braces can be dropped)
Snoc is
    fn (List a)    a => List a;
Snoc == {
    fn Nil         y -> Cons y Nil;
    fn (Cons x xs) y -> Cons x (Snoc xs y);
};

# matching style C
Snoc is
    List a    => a => List a;
Snoc == {
    Nil       -> y -> Cons y Nil;
    Cons x xs -> y -> Cons x (Snoc xs y);
};
# NOTE that this wouldn't work if the args to Snoc came
#      in the other order, because its fully explicit
#      form is really
Snoc == {
    fn Nil         -> { fn y -> Cons y Nil };
    fn (Cons x xs) -> { fn y -> Cons x (Snoc xs y) };
};
# whereas the other order makes no sense:
Snoc == {
    fn y -> { fn Nil         -> Cons y Nil };
    fn y -> { fn (Cons x xs) -> Cons x (Snoc y xs) };
};

# Example where we need multi-argument patterns
Append is
    fn (List a)    (List a) => List a;
Append == {
    fn xs          Nil      -> xs;
    fn Nil         ys       -> ys;
    fn (Cons x xs) ys       -> Cons x (Append xs ys);
};

# uncurried
# recall that , has higher precedence than ->
Append is
    List a, List a => List a;
Append == {
    xs,        Nil -> xs;
    Nil,       ys  -> ys;
    Cons x xs, ys  -> Cons x (Append (xs, ys));
};

# use of match operator
Append (List a) (List a) is List a;
Append xs ys == ys match {
    Nil -> xs;
    ys  -> xs match {
        Nil       -> ys;
        Cons x xs -> Cons x (Append xs ys);
    };
};

# Is <exp1> match <exp2> really any different from
# <exp1> \ <exp2> with the following definition?
a \ (a => b) is b;
x \ f == f x;
# there may be a problem with bidirectionality...

Append xs ys == ys \ {
    Nil -> xs;
    ys  -> xs \ {
        Nil       -> ys;
        Cons x xs -> Cons x (Append xs ys);
    };
};

# Note that patterns are just expressions as far as parsing
# is concerned.  The keyword "fn", if present, just stands for the
# anonymous function itself in the pattern for each case.  So for
# instance we have
List a `Append` List a is List a;
Append == {
    xs        `fn` Nil -> xs;
    Nil       `fn` ys  -> ys;
    Cons x xs `fn` ys  -> Cons x (xs `Append` ys);
};
# by the way, this is why
#   Add3 == { x y z -> x + y + z }
# makes no sense and is illegal; it would have to mean
#   Add3 == { (x y) z -> x + y + z }
# which is silly.  Instead, you must write
#   Add3 == { fn x y z -> x + y + z }
# which is perfectly sensible and of course means
#   Add3 == { ((fn x) y) z -> x + y + z }

# where clause syntax
# Style A
Append is List a => List a => List a;
Append xs Nil == xs;
Append xs ys == A xs where A == {
    Nil -> ys;
    Cons x xs -> Cons x (A xs);
};
# Style B
# you can use multiple declarations enclosed in braces
Append is List a => List a => List a;
Append xs Nil == xs;
Append xs ys == A xs where {
    A Nil         == ys;
    A (Cons x xs) == Cons x (A xs);
};
# Style C (using conditional)
Append is List a => List a => List a;
Append xs ys == xs if ys = Nil
              | A xs
where {
    A Nil         == ys;
    A (Cons x xs) == Cons x (A xs);
};

# More conditional syntax
# this is not a special form of pattern (as in Haskell); instead,
# (<exp> if <exp> | <exp>) is just another kind of expression, with
# the correct associativity to make this look nice.
Sgn is Int => Int;
Sgn n == 1      if n > 0
       | -1     if n < 0
       | 0; 



### Datatype declarations

data Color == { Red; Green; Blue };
data Maybe a == { Nothing; Just a };
data Either a b == { Left a; Right b };

# more explicit form (necessary if we have index refinements running
# around, or if we want "generalized ADTs")

data Color == { Red is Color; Green is Color; Blue is Color };
data Maybe a == {
    Nothing is Maybe a;
    Just a  is Maybe a;
};
data Either a b == {
    Left a  is Either a b;
    Right b is Either a b;
};

# equivalent:
data Maybe a == {
    Nothing is Maybe a;
    Just    is a => Maybe a;
};
data Either a b == {
    Left  is a => Either a b;
    Right is b => Either a b;
};

# These "constructor declarations" must be curried functions where
# the final result type is an instance of the datatype being declared
# (but see below for relaxed rules for datasort refinements)

# legal:
data D a b == {
    C is (a, b) => D a b;
};
# bogus:
data D a b == {
    C is D a b => (a, b);
};
# legal (polymorphic recursion):
data D a b == {
    C is D (a, b) b => D a b;
};
# legal (generalized ADT):
data D a b == {
    C is b => D Int b;
};
# legal but strange (this is an existential type):
data D == {
    C is (a, b) => D;
};
# legal (WHEN constructors are given EXPLICIT RESULT TYPES, the
# type declaration is treated as closed):
data D a b == {
    C is (b, a) => D b a;
};
# alpha-varied to make it clearer that the a,b in the constructor
# declaration have nothing to do with the a,b in the datatype part:
data D a b == {
    C is (t, u) => D t u;
};



### Declaration of the standard list datatype

# Style A
# $ is a letter.  any symbol ending with : is right-associative
data List a == { $; a : List a };
# Style B (constructor-level function-ish)
data List == a -> { $; a : List a };

# Style A
Map f $      == $;
Map f (x:xs) == f x : Map f xs;
# Style B
Map f == {
    $      -> $;
    x : xs -> f x : Map f xs;
};

# non-datatype type declarations
# Style A
type PairList a == List (a, a)
# Style B (constructor-level function)
type PairList == a -> List (a, a)



### Lazy datatypes
# This is "even" style a la Wadler

# Style A
data Stream a ~= { $$; a :: Stream a };
# Style B
data Stream == a ~> { $$; a :: Stream a };

# Style A
SMap f $$      ~= $$;
SMap f (x::xs) ~= f x :: SMap f xs;
# Style B
SMap f == {
    $$ ~> $$;
    x :: xs ~> f x :: SMap f xs;
};

# You can only use ~= or ~> if the RHS is statically a lazy datatype
# Remember that we are a CBV language, so
Delay is Stream a => Stream a;
Delay x ~= x;
# does NOT do what its name purports.  If delay is added to the language
# it must be a special form.

# Along these lines, recall that uppercase (proper) names stand for
# EXPRESSIONS, not VALUES, so the following DOES do what you want:
Print is String => (); # unit type
PrintLn is ();
PrintLn == Print "\n";

PrintGreeting is ();
PrintGreeting == do {
    Print "Hello, world!";
    PrintLn;
    Print "This appears on the next line.";
    PrintLn;
};



### The `...` syntax

val xs == (1:2:3:$) `Append` (4:5:6:$);

List a `Append` List a is List a;
$      `Append` ys == ys;
(x:xs) `Append` ys == x : (xs `Append` ys);


### Sneaky uses of `...`

Append is
    List a `fn` List a => List a;
Append == {
    $      `fn` ys -> ys;
    (x:xs) `fn` ys -> x : (xs `Append` ys);
};

# even sneakier

# Style A
FoldR (a => b => b) (List a) b is b;
FoldR f $      y == y;
FoldR f (x:xs) y == f x (FoldR f xs y);

# Style B
List a `FoldR (a => b => b)` b is b;
$      `FoldR f` y == y;
(x:xs) `FoldR f` y == f x (xs `FoldR f` y);

# Style C (for the truly perverse)
List a `FoldR (a `fn` b => b)` b is b;
$      `FoldR f` y == y;
(x:xs) `FoldR f` y == x `f` (xs `FoldR f` y);



### Stuff for the standard prelude

# Application forms
x \ f == f x;
f /: x == f x;
xs \\ f == Map f xs;
f //: xs == Map f xs;

(xs \@ f)  y == xs `FoldR f` y;
(f /@: xs) y == y `FoldL f` xs;

# We have for instance
(1:2:3:$) \@ f  == x -> 1 `f` (2 `f` (3 `f` x));
f /@: (1:2:3:$) == x -> ((x `f` 1) `f` 2) `f` 3;

# If we allow . as a symbol
f . g == x -> f (g x);



### More examples

Fact Int is Int;
# Style A
Fact 0 == 1;
Fact n == n * Fact (n-1);
# Style B
Fact == {
    0 -> 1;
    n -> n * Fact (n-1);
};
# Style C
Fact n == n match {
    0 -> 1;
    k -> k * Fact (k-1);
};
# Style D
Fact n == 1 if n = 0
        | n * Fact (n-1);

# ? and ! are letters
Even? Int is Int;
Even? n == E? x where {
    val x is Int == n   if n >= 0
                  | -n;

    E? Int and O? Int is Int;
    E? n == True        if n = 0
          | O? (n-1);
    O? n == False       if n = 0
          | E? (n-1);
};

let {
    Even? and Odd? is Int => Int;
    Even? n == E? n' where val n' is Int == n if n >= 0 | -n;
    Odd? n  == O? n' where val n' is Int == n if n >= 0 | -n;
} where {
    E? and O? is Int => Int;
    E? n == True        if n = 0
          | O? (n-1);
    O? n == False       if n = 0
          | E? (n-1);
};



### Datasort refinements
# Using the same constructor name in multiple datatype
# declarations within the same scope means we're declaring
# datasorts.
data Nat == { Zero; Succ Nat };
data Even == { Zero; Succ Odd };
data Odd == Succ Even;

# Style A
Succ2 Even is Even;
Succ2 Odd  is Odd;
Succ2 n    == Succ (Succ n);

# Style B
Succ2 is Even => Even;
Succ2 is Odd  => Odd;
Succ2 == n    -> Succ (Succ n);

# Style C
Succ2 is {
    Even => Even;
    Odd  => Odd;
};
Succ2 ==
    n    -> Succ (Succ n);

# Style A
Pred Nat  is Nat;
Pred Even is Nat;
Pred Odd  is Even;
Pred Zero     == Zero;
Pred (Succ n) == n;

# Style B
Pred is {
    Nat  => Nat;
    Even => Nat;
    Odd  => Even;
};
Pred == {
    Zero   -> Zero;
    Succ n -> n;
};

# Style C
Pred is (Nat => Nat) /\ (Even => Nat) /\ (Odd => Even);
Pred == { Zero -> Zero; Succ n -> n };



### Index refinements
# Maybe kinds can be inferred

# Style A
data List Type Nat is Type;
data List a n == {
    Nil is List a 0;
    Cons a (List a n) is List a (n+1);
};
# Style B
data List is Type => Nat => Type;
data List == a -> n -> {
    Nil  is List a 0;
    Cons is a => List a n => List a (n+1);
};
# Style C
data List is fn Type Nat => Type;
data List == fn a n -> {
    Nil  is fn => List a 0;
    Cons is fn a (List a n) => List a (n+1);
};



### Existential types

data Closure a b == MkClosure env (env => a => b);

# Recall that the above is just an abbreviation for
data Closure a b == {
    MkClosure is env => (env => t => u) => Closure t u;
};
# and now it's easy to see why this is an existential type...
# essentially the constructor MkClosure is polymorphic in env
# (because whenever we declare the type of something, it's
# polymorphic in any type variables that aren't bound by enclosing
# scopes)



### Polymorphic recursion

data Balanced a == { Leaf a; Node (Balanced (a, a)) };



### Higher kinds

data SillyTree m == { Leaf Int; Node (m (SillyTree m)) };
type Balanced2 == SillyTree (fn a -> (a, a));
type Balanced2 == SillyTree (a -> a, a);