/*
This is a tutorial and introduction to the Sage Language. A good
familiarity with programming in conventional languaegs is assumed,
specifically knowledge of ML or an ML variant would be helpful.
Sage can be described as an extended version of ML but
there are different names for ML analogs in Sage. Specifically
there are three new innovations:
- Type Refinements
- Dynamic Type
- Pure Type system
For this overview of Sage we use the interactive system which is launched by not
including any files in the invocation of Sage. The command prompt is a '#' sign
and Sage responds with the type and the result of evaluation. Later in the tutorial
these responses are elided in favor of brevity.
There exists a batch version of Sage in which commands are written
to a file, (ie. file.sage) and run by calling the Sage program with that file as the
last argument (ie. % sage file.sage)
*/
/* BASICS
This is a comment. Comments in Sage are begun with a "/*"
and ended with "*/".
While more useful for batch files; this also holds for the interactive system.
In Sage commands are terminated by ;;
*/
# 1 + 2;;
Type: (Refine Int (fn (z:Int) => (inteq z (add 1 2))))
Evaluation: 3
/*The type of (1+2) is not merely Int but the singleton type for (1+2). All integers that
evaluate to the value 3. This singleton integer is denoted by the Refine
with predicate testing any integer with equality to (add 1 2)*/
# (1 + 2) - 4;;
Type: (Refine Int (fn (z:Int) => (inteq z (sub (add 1 2) 4))))
Evaluation: -1
# eq (11 < 10) true;;
Type: Bool
Evaluation: false
/*eq is a prefix notation for equality. The two terms compared for
equality are (11 < 10) and true. Many boolean operators have prefix
notation and a few have infix notation like '&&' and '||'*/
# not (true || false);;
Type: (Refine Bool (fn (c:Bool) => (iff c (not (or true false)))))
Evaluation: false
# let xor (x1:Bool) (x2:Bool) = ((x1 && (not x2)) || ((not x1) && x2));;
Binding for: xor
Type: (x1:Bool -> x2:Bool ->
(Refine Bool
(fn (z:Bool) =>
(iff z (or (and x1 (not x2)) (and (not x1) x2))))))
Evaluation: (fn (x1:Bool) (x2:Bool) =>
(or (and x1 (not x2)) (and (not x1) x2)))
# xor true false;;
Type: (Refine Bool
(fn (z:Bool) =>
(iff z (or (and true (not false)) (and (not true) false)))))
Evaluation: true
/*
Here is a way to declare the increment function _without_ naming it.
*/
# fn (x:Int) => (x + 1);;
Type: (x:Int ->
(Refine Int (fn (z:Int) => (inteq z (add x 1)))))
Evaluation: (fn (x:Int) => (add x 1))
/*
The functions, fn, do not require types attached to them but as with all
signatures this helps clarify to the compiler the intention of the
programmer. This becomes more helpful after user-refined types are
introduced. "fn" may have more than one argument.
*/
/*
Here is an example of function application.
*/
# ((fn (x:Int) => (x+1)) 1);;
Type: (Refine Int (fn (z:Int) => (inteq z (add 1 1))))
Evaluation: 2
/*
In order to reduce repetion the let construct allows you to bind
a name inc, to a term (x + 1) in the term (inc (inc 3)).
The inc binding has a scope limited to the term between the keyword
'in' and the ending ;;
Arguments bindings can be placed before the '=' sign.
*/
# let inc = (fn (x:Int) => x + 1) in (inc (inc 3));;
Type: (Refine Int
(fn (z:Int) =>
(inteq z (add ((fn (x':Int) => (add x' 1)) 3) 1))))
Evaluation: 5
# let inc (x:Int) = x+1 in (inc (inc 3));;
Type: (Refine Int
(fn (z:Int) =>
(inteq z (add ((fn (x':Int) => (add x' 1)) 3) 1))))
Evaluation: 5
/*
If one wishes to bind a name to a term for the remainder of the file a
slightly different syntax is used. There is no keyword 'in'.
*/
# let inc (x:Int) = x+1;;
Binding for: inc
Type: (x':Int ->
(Refine Int (fn (z:Int) => (inteq z (add x' 1)))))
Evaluation: (fn (x':Int) => (add x' 1))
# (inc (inc 3));;
Type: (Refine Int (fn (z:Int) => (inteq z (add (inc 3) 1))))
Evaluation: 5
/*Occassionally it would be helpful to give recursive definitions of functions*/
# let rec fib (n:Int):Int =
if [Int] ((n=1) || (n = 0))
then 1
else (fib (n-1)) + (fib (n-2));;
Binding for: fib
Type: (n:Int -> Int)
Evaluation: (fix (n:Int -> Int)
(fn (fib:(n:Int -> Int)) (n:Int) =>
(IF Int (or (inteq n 1) (inteq n 0))
(fn
(_:(Refine Unit
(fn (u1:Unit) =>
(or (inteq n 1) (inteq n 0))))) =>
1)
(fn
(_:(Refine Unit
(fn (u2:Unit) =>
(not (or (inteq n 1) (inteq n 0)))))) =>
(add (fib (sub n 1)) (fib (sub n 2)))))))
# (fib 3)+(fib 4);;
Type: (Refine Int (fn (z:Int) => (inteq z (add (fib 3) (fib 4)))))
Evaluation: 8
# (fib 1);;
Type: Int
Evaluation: 1
/*
To describe the type of a function a type constructor is introduced. the arrow:
eg.
x:Int -> Int
or simply Int -> Int
*/
# let case_app (x:Int) (f:(Int -> Int)) (g:(Int -> Int))=
if [Int] (x >= 0)
then (f x)
else (g x);;
Binding for: case_app
Type: (x:Int -> f:(Int -> Int) -> g:(Int -> Int) -> Int)
Evaluation: (fn (x:Int) (f:(Int -> Int)) (g:(Int -> Int)) =>
(IF Int (geq x 0)
(fn
(_:(Refine Unit
(fn (u1:Unit) => (geq x 0)))) =>
(f x))
(fn
(_:(Refine Unit
(fn (u2:Unit) => (not (geq x 0))))) =>
(g x))))
/* Constants.
The increment function uses the '+' operator and the numeral '1'. These are not
defined in the basic language but are one of many constants built into Sage.
Others that have already occured include the comparison function '>' and
if/then control term seen in the definition of fib. The '||', '&&' and 'not'
constants were used in the defintion of xor.
I will introduce the more unusual constants here.
Unit is a type with populated by a single term, unit. It is essentially a
dummy type and term used to create 'thunks', or delay evaluation until
run time.
*/
#let cur_time = . . . ;; /*The system time function should be here.*/
# let time (u:Unit) = cur_time;;
Binding for: time
Type: (u:Unit ->
(Refine (Refine Int (fn (x':Int) => (inteq x' 1)))
(fn (svar:(Refine Int (fn (x':Int) => (inteq x' 1)))) =>
(eq svar cur_time))))
Evaluation: (fn (u:Unit) => cur_time)
/*
The constant '*' is the type of types. The following function takes in types
and returns and integer constant.
The constant IF/ if [T] b then s else t
T describes the type of s and t for the compiler.
Because the two branches of an if statement 's' & 't' may have different exact
types the compiler presumes that the greatest common type has type
dynamic unless it can prove otherwise or you give it a hint. That hint is adding
the '[T]'.
*/
# let is_int_type (X:*) = if [Bool] (eq X Int) then true else false;;
Binding for: is_int_type
Type: (X:* -> Bool)
Evaluation: (fn (X:*) =>
(IF Bool (eq X Int)
(fn
(_:(Refine Unit
(fn (u1:Unit) => (eq X Int)))) =>
true)
(fn
(_:(Refine Unit
(fn (u2:Unit) => (not (eq X Int))))) =>
false)))
/* As Sage does not yet do more than a bare minimum of type inference,
without a signature, the argument x without a clarifying type has the
Dynamic type. The following two functions are exactly the same.
*/
# fn x => (x + 1);;
Type: (x:Dynamic ->
(Refine Int
(fn (z:Int) =>
(inteq z
(add
(cast (Refine Dynamic (fn (svar:Dynamic) => (eq svar x))) Int x)
1)))))
Evaluation: (fn (x:Dynamic) =>
(add
(cast (Refine Dynamic (fn (svar:Dynamic) => (eq svar x))) Int x)
1))
# fn (x:Dynamic) => (x + 1);;
(Identical to above.)
/*
Dynamic:
Dynamic is a constant type which has the property that any type can be
cast to Dynamic and
that the type Dynamic can be cast to any type (with a dynamic check).
This kind of function declaration is useful when prototyping a
program.
*/
# let toInt (x:Dynamic) :Int = x as Int;;
Binding for: toInt
Type: (x:Dynamic ->
(Refine Int
(fn (svar:Int) =>
(eq svar
((fn (x':Int) => x')
(cast
(Refine Dynamic (fn (svar':Dynamic) => (eq svar' x)))
Int x))))))
Evaluation: (fn (x:Dynamic) =>
(cast
(Refine Dynamic (fn (svar:Dynamic) => (eq svar x)))
Int x))
/* The cast constant which gives the term the a new type
with the caveat that if the term proves to be of a different type; there will be
a dynamic failure during runtime. */
let toInt (x:Dynamic) : Int = cast Int x;;
/*
Another form of cast is the 'as' qualifier. The term 'as' differs only during
compile time where a type relation between the term's type (x) and the new
type is found.
*/
let toInt (x:Dynamic) = x as Int;;
/*
The following function is an example of a wrapper function
which tests a predicate. The failure function simply gives a
cast which will fail at runtime because true is not of type Int.
*/
#let fail_fun (x:*) = cast Bool x true;;
Binding for: fail_fun
Type: (x:* -> x)
Evaluation: (fn (x:*) => (cast Bool x true))
# let safe_app (x:Int) (f:(Int -> Int)) =
if [Int] (x > 0)
then (f x)
else fail_fun Int;;
Binding for: safe_app
Type: (x:Int -> f:(Int -> Int) -> Int)
Evaluation: (fn (x:Int) (f:(Int -> Int)) =>
(IF Int (gt x 0)
(fn
(_:(Refine Unit
(fn (u1:Unit) => (gt x 0)))) =>
(f x))
(fn
(_:(Refine Unit
(fn (u2:Unit) => (not (gt x 0))))) =>
(fail_fun Int))))
/* On parentheses:
One can always surround a term with parentheses to disambiguate a term.
This is especially useful when you have multiple terms in the clause of
an if/then/else statement or need to distinguish the arguments as you
are mixing infix and prefix operators.
*/
/*On Datatype declarations
Datatype declarations are built in 'sum' constructors that
not only declare the datatype, type (in this case List)
but also the constructor for possible members (Null and Unit).
*/
# datatype List (T:*) = Null of (u:Unit) | Cons of (x:T) (r:(List T));;
Binding for: List
Type: (* -> *)
Evaluation: (fix (* -> *)
(fn (List:(* -> *)) (T:*) =>
(Z:* -> Nullfn:(u:Unit -> Z) ->
Consfn:(x:T -> r:(List T) -> Z) -> Z)))
Binding for: caseList
Type: (T:* -> v:(List T) ->
(Refine (List T) (fn (svar:(List T)) => (eq svar v))))
Evaluation: (fn (T:*) (v:(List T)) => v)
Binding for: Null
Type: (T:* -> u:Unit -> Z:* -> Nullfn:(u':Unit -> Z) ->
Consfn:(x:T -> r:(List T) -> Z) -> Z)
Evaluation: (fn (T:*) (u:Unit) (Z:*) (Nullfn:(u':Unit -> Z))
(Consfn:(x:T -> r:(List T) -> Z)) => (Nullfn u))
Binding for: Cons
Type: (T:* -> x:T -> r:(List T) -> Z:* -> Nullfn:(u:Unit -> Z) ->
Consfn:(x':T -> r':(List T) -> Z) -> Z)
Evaluation: (fn (T:*) (x:T) (r:(List T)) (Z:*)
(Nullfn:(u:Unit -> Z))
(Consfn:(x':T -> r':(List T) -> Z)) => (Consfn x r))
/*
Null is the name of the first possible constructor of
List and contains a field of type Unit.
Cons is the name of the second possible constructor of list
and contains a field of type T and List T.
Elements constructed with Null are empty lists.
Elements constrcuted with Cons are lists with
at least the item x of type T in it.
Here are the constructors in use. The first is an integer list
size 0 and the second is an integer list size 1 (with the 5 object)
*/
# let null = Null Int unit;;
Binding for: null
Type: (Z:* -> Nullfn:(u:Unit -> Z) ->
Consfn:(x:Int -> r:(List Int) -> Z) -> Z)
Evaluation: (fn (Z:*) (Nullfn:(u:Unit -> Z))
(Consfn:(x:Int -> r:(List Int) -> Z)) =>
(Nullfn unit))
q
# let l1 = Cons Int 5 null;;
Binding for: l1
Type: (Z:* -> Nullfn:(u:Unit -> Z) ->
Consfn:(x:Int -> r:(List Int) -> Z) -> Z)
Evaluation: (fn (Z:*) (Nullfn:(u:Unit -> Z))
(Consfn:(x:Int -> r:(List Int) -> Z)) =>
(Consfn 5
(fn (Z':*) (Nullfn':(u:Unit -> Z'))
(Consfn':(x:Int -> r:(List Int) -> Z')) =>
(Nullfn' unit))))
/*
Finally after using the datatype constructor we can write
functions such as length quite easily using the builtin case constructor
which is named the same as the data type with the word 'case' prefixed on it.
For example caseList is the case constructor for the datatype list.
To be explicit, the first argument to the caseList case discriminator
is the the type of the list (T), followed by the actual list (l), followed by the
return type of the caseList function (Int), and finally the functions to be called
for each possible case.
*/
# let rec length (T:*) (l:List T):Int =
(caseList T l Int
(fn u => 0)
(fn x r => 1 + (length T r)));;
Binding for: length
Type: (* -> (List _) -> Int)
Evaluation: . . .
# length Int null;;
Type: Int
Evaluation: 0
# length Int l1;;
Type: Int
Evaluation: 1
/* On Type declarations
Shorthands for types can be declared.
*/
# let IntFun = Int -> Int;;
Binding for: IntFun
Type: *
Evaluation: (Int -> Int)
# let app_switch (x:Int) (f:IntFun) (g:IntFun) = if [Int] (x > 0) then (f x) else (g x);;
Binding for: app_switch
Type: (x:Int -> f:IntFun -> g:IntFun -> Int)
Evaluation: . . .
/* On Refinement Types -
Recall fib.
The old definition was fine for positive numbers but diverges for
numbers below zero. We would like to restrict the input of the function
to be only positive integers. To enforce this restriction we can construct
a refinement type; a type with restrictions on it.
*/
# let Pos = {x:Int | x >= 0};;
Binding for: Pos
Type: *
Evaluation: (Refine Int (fn (x:Int) => (geq x 0)))
# let rec safe_fib (n:Pos) : Pos =
if [Pos] (n < 2)
then 1
else ((safe_fib (n-1)) + (safe_fib (n-2)));;
Binding for: safe_fib
Type: (Pos -> Pos)
Evaluation: (fix (Pos -> Pos)
(fn (safe_fib:(Pos -> Pos)) (n:Pos) =>
(IF Pos (lt n 2)
(fn
(_:(Refine Unit
(fn u1:Unit) => (lt n 2)))) =>
1)
(fn
(_:(Refine Unit
(fn (u2:Unit) => (not (lt n 2))))) =>
(add (safe_fib (sub n 1)) (safe_fib (sub n 2)))))))
# safe_fib 4;;
Type: Pos
Evaluation: 5
# safe_fib (0 - 1);;
Warning:
:1.1:
The term (sub 0 1)
has type (Refine Int (fn (z:Int) => (inteq z (sub 0 1))))
which is not a subtype of expected type Pos
Type: Pos
/*Refinements in conjunction with the datatype construct are a powerful tool.
Here is the example of an ordered list.
*/
# datatype OrderedList (lo:Int) =
ONull of (u:Unit)
| OCons of (h:Int.(lo <= h)) (t:(OrderedList h));;
Binding for: OrderedList
Type: (Int -> *)
Evaluation: . . .
Binding for: caseOrderedList
Type: (lo:Int -> v:(OrderedList lo) ->
(Refine (OrderedList lo)
(fn (svar:(OrderedList lo)) => (eq svar v))))
Evaluation: (fn (lo:Int) (v:(OrderedList lo)) => v)
Binding for: ONull
Type: (lo:Int -> u:Unit -> Z:* -> ONullfn:(u':Unit -> Z) ->
OConsfn:(h:(Refine Int (fn (h:Int) => (leq lo h))) ->
t:(OrderedList h) -> Z) -> Z)
Evaluation: . . .
Binding for: OCons
Starting Simplify with Command: Simplify -nosc
Type: (lo:Int -> h:(Refine Int (fn (h:Int) => (leq lo h))) ->
t:(OrderedList h) -> Z:* -> ONullfn:(u:Unit -> Z) ->
OConsfn:(h':(Refine Int (fn (h':Int) => (leq lo h'))) ->
t':(OrderedList h') -> Z) -> Z)
Evaluation: . . .
/*
Together with the 'Above' type declared below, the merge algorithm
can be written ensuring that the list returned by merge is ordered.
*/
# let Above (x:Int):* = (y:Int.x<=y);;
Binding for: Above
Type: (x:Int ->
(Refine *
(fn (svar:*) =>
(eq svar (Refine Int (fn (y:Int) => (leq x y)))))))
Evaluation: (fn (x:Int) => (Refine Int (fn (y:Int) => (leq x y))))
# let rec merge (lo:Int)
(lo1:Above lo)
(l1:OrderedList lo1)
(lo2:Above lo)
(l2:OrderedList lo2) :
(OrderedList lo) =
caseOrderedList lo1 l1 (OrderedList lo)
(fn u => l2)
(fn h1 t1 =>
caseOrderedList lo2 l2 (OrderedList lo)
(fn u => l1)
(fn h2 t2 =>
if[OrderedList lo] h1 < h2 then
(OCons lo h1
(merge h1 h1 t1 h2 (OCons h2 h2 t2)))
else
(OCons lo h2
(merge h2 h2 t2 h1 (OCons h1 h1 t1)))
)
)
;;
Binding for: merge
Type: (Int -> (Above _) -> (OrderedList _') -> (Above _) ->
(OrderedList _''') -> (OrderedList _))
Evaluation: . . .
/*
Refinements are a powerful tool to automatically check
restrictions on input and output of the tools but can also be used to
enforce unrelated requirements for functions.
Imagine that there exists a I/O function named read_int
*/
# let read_Int (i:Unit) :Int = 0;; /*Dummy Function. Should be system defined*/
Binding for: read_Int
Type: (i:Unit -> (Refine Int (fn (svar:Int) => (eq svar 0))))
Evaluation: (fn (i:Unit) => 0)
# let Signal = Int;;
Binding for: Signal
Type: *
Evaluation: Int
#let sig (u:Unit) = (read_Int unit) as Signal;;
Binding for: sig
Type: (u:Unit ->
(Refine Signal
(fn (svar:Signal) => (eq svar (read_Int unit)))))
Evaluation: (fn (u:Unit) => (read_Int unit))
# let done (s:Signal) = (s > 0);;
Binding for: done
Type: (s:Signal ->
(Refine Bool (fn (b:Bool) => (iff b (gt s 0)))))
Evaluation: (fn (s:Signal) => (gt s 0))
# let fragile_fun (x:{u:Unit|(done (sig unit))}) = x;;
Binding for: fragile_fun
Type: (x:(Refine Unit (fn (u:Unit) => (done (sig unit)))) ->
(Refine (Refine Unit (fn (u:Unit) => (done (sig unit))))
(fn
(svar:(Refine Unit (fn (u:Unit) => (done (sig unit))))) =>
(eq svar x))))
Evaluation: (fn
(x:(Refine Unit (fn (u:Unit) => (done (sig unit))))) =>
x)
# fragile_fun unit;;
Type: . . .
Evaluation:
Failed cast:
From: Unit
To: (Refine Unit (fn (u:Unit) => (done (sig unit))))
On: unit
With label: none
/*
As read_Int depends on program independent input,
the typechecker cannot statically determine that a call to fragile_fun
will always occur when sig > 0. Instead, it inserts a dynamic check
which acts as a gatekeeper for the fragile function.
*/
/* On dynamic -
Occasionally there are times when determining the most specific type
may be onerous to determine and you are willing to accept a number of
runtime checks. For this there exists the type Dyanmic. Any type can
be upcast to Dynamic and the Dynamic type can be implicitly downcast
(via a dynamic check) to any type.
For example imagine that the read function is not type specific.
There is no way of knowing what the read function will return. An int,
a character, or a bool. In this case it might be best to give the
read function the following signature:
*/
let read (u:Unit) : Dynamic= . . . ;; /*Should be system dependent */
let readInt (u:Unit) = (read u) as Int;;
/* On Pure type systems -
As Sage is a language with a united type and term language, it permits
functions on types. One can imagine that given that the result of the read
function is in ascii form, an accurate Type for read will require
a type dependent on the input.
*/
# let Char = Int;;
Binding for: Char
Type: *
Evaluation: Int
# let ReadTy (x:Int) : * =
if [*] (x >= 48) && (x <= 57) then Int
else
(if [*] (x >= 65) && (x <= 90) then Char
else Dynamic);;
Binding for: ReadTy
Type: . . .
Evaluation: . . .
# let read (u:Unit) = let x = ( . . . ) in [x as (ReadTy x)];;
/* On coding checks
- full type signatures fn (x:Int) : Int
It is always wise to incorporate checks into the signatures.
Merge was a complicated function
which isn't obvious to write. Here is an early incarnation of merge:
*/
#let rec merge (lo:Int)
(lo1: Int)
(l1:OrderedList lo1)
(lo2: Int)
(l2:OrderedList lo2) :
(OrderedList lo) =
caseOrderedList lo1 l1 (OrderedList lo)
(fn u => l2)
(fn h1 t1 =>
caseOrderedList lo2 l2 (OrderedList lo)
(fn u => l1)
(fn h2 t2 =>
if[OrderedList lo] h1 < h2 then
(OCons lo h1
(merge h1 h1 t1 h2 (OCons h2 h2 t2)))
else
(OCons lo h2
(merge h2 h2 t2 h1 (OCons h1 h1 t1)))
)
)
;;
Binding for: merge
Warning:
:16.-363:
The term l2
has type (Refine (OrderedList lo2)
(fn (svar:(OrderedList lo2)) => (eq svar l2)))
which is not a subtype of expected type (OrderedList lo)
/*
The warning from Sage simply says that the term l2 has the singleton type
(OrderedList lo2) which is not a subtype of (OrderedList lo). One example of
an ordered list which is not a subtype of lo is where lo2 = lo1 - 1.
This pinpointing of the problem, with a little practice, allows you to write
more accurate types to refine your code. Thus resulting in the
'Above' type and the code first presented for the merge function.
*/
/* Mini Reference:
Here is the entire list of constants in Sage.
They include:
'unit','n','true','false' - term constants (where n is an integer)
'Unit','Int','Bool', 'Dynamic'- type constants
'*' - The type of a type.
'+','-','=','>','<','>=','<=' - binary infix arithmatic operators
'not','eq','or','and'- prefix boolean operators
'&&','||' - infix boolean operators
'fix' T (fn (x:T) => t) - recursion operator
'if' t1 'then' t2 'else' t3 - the an if control flow command
'cast' T t - which dynamically checks that the type of the term t is T and
changes the compile time type to T.
*/