Homework #7 Questions

Using the `fullsimple` checker

Q: What is fullsimple ? Another programming language like SASyLF ?

Q: It's the simply typed lambda calculus with most of the various extensions in it from Chapter 11: Nat, Bool, Unit, fix, records, variants.

You run it the same way we ran fulluntyped for Homework #3. For example:


weise 36 % cd ~/cs732/checkers/fullsimple
weise 37 % cat test.f
/* Examples for testing */

  
 lambda x:<a:Bool,b:Bool>. x;
 

"hello";

unit;

lambda x:A. x;

let x=true in x;

timesfloat 2.0 3.14159;

{x=true, y=false}; 
{x=true, y=false}.x;
{true, false}; 
{true, false}.1; 


lambda x:Bool. x;
(lambda x:Bool->Bool. if x false then true else false) 
  (lambda x:Bool. if x then false else true); 

lambda x:Nat. succ x;
(lambda x:Nat. succ (succ x)) (succ 0); 

T = Nat->Nat;
lambda f:T. lambda x:Nat. f (f x);

weise 38 % ./f test.f
(lambda x:<a:Bool,b:Bool>. x)
  : <a:Bool,b:Bool> -> <a:Bool, b:Bool>
"hello" : String
unit : Unit
(lambda x:A. x) : A -> A
true : Bool
6.28318 : Float
{x=true, y=false} : {x:Bool, y:Bool}
true : Bool
{true, false} : {Bool, Bool}
true : Bool
(lambda x:Bool. x) : Bool -> Bool
true : Bool
(lambda x:Nat. (succ x)) : Nat -> Nat
3 : Nat
T :: *
(lambda f:T. lambda x:Nat. f (f x)) : T -> Nat -> Nat
weise 39 % cd ../../src/homework7
weise 40 % pwd
/afs/cs.uwm.edu/users/classes/cs732/src/homework7
weise 41 % cat table.f
OptionalNat = <none:Unit, some:Nat>;

Table = Nat -> OptionalNat;

emptyTable = lambda n:Nat . <none=unit> as OptionalNat;

equal = fix (lambda eq:Nat->Nat->Bool .
              lambda m:Nat . lambda n:Nat .
                if iszero m then iszero n
                else if iszero n then false
                else eq (pred m) (pred n));

extendTable =
  lambda t:Table . lambda m:Nat . lambda v:Nat .
    lambda n:Nat .
      if equal n m then <some=v> as OptionalNat
      else t n;

t = extendTable (extendTable emptyTable 3 9) 5 25;

case t(2) of
       <none=u> ==> 999
     | <some=v> ==> v;

case t(3) of
       <none=u> ==> 999
     | <some=v> ==> v;


weise 42 % ~/cs732/checkers/fullsimple/f table.f
OptionalNat :: *
Table :: *
emptyTable : Nat -> OptionalNat
equal : Nat -> Nat -> Bool
extendTable : Table -> Nat -> Nat -> Nat -> OptionalNat
t : Nat -> OptionalNat
999 : Nat
9 : Nat

Homework #7 Questions

Using the fullsimple checker

Using the `fullsimple` checker