Seminar

README.md

@@ -1,6 +1,8 @@
 # LCI
 
-[Report](report/document.pdf) is located in the [report/](report/) folder
+[Report](report/document.pdf) is located in the [report/](report/) folder.
+
+[Seminar Slides](seminar/document.pdf) are located in the [seminar/](seminar/) folder.
 
 ## To install prerequisites
 

bin/dune

@@ -1,26 +1,36 @@
 (executable
-  (name miniFunInterpreter)
-  (public_name miniFunInterpreter)
-  (libraries miniFun
-             clap)
-  (package miniFun)
-  (modes byte exe)
-  )
+ (name miniFunInterpreter)
+ (public_name miniFunInterpreter)
+ (libraries miniFun
+            clap)
+ (package miniFun)
+ (modes byte exe)
+)
 
 (executable
-  (name miniImpInterpreter)
-  (public_name miniImpInterpreter)
-  (libraries miniImp
-             clap)
-  (package miniImp)
-  (modes byte exe)
-  )
+ (name miniFunPolyInterpreter)
+ (public_name miniFunPolyInterpreter)
+ (libraries miniFun
+            clap)
+ (package miniFun)
+ (modes byte exe)
+)
+
 
 (executable
-  (name miniImpInterpreterReg)
-  (public_name miniImpInterpreterReg)
-  (libraries miniImp
-             clap)
-  (package miniImp)
-  (modes byte exe)
-  )
+ (name miniImpInterpreter)
+ (public_name miniImpInterpreter)
+ (libraries miniImp
+            clap)
+ (package miniImp)
+ (modes byte exe)
+)
+
+(executable
+ (name miniImpInterpreterReg)
+ (public_name miniImpInterpreterReg)
+ (libraries miniImp
+            clap)
+ (package miniImp)
+ (modes byte exe)
+)

bin/miniFunPolyInterpreter.ml

@@ -0,0 +1,118 @@
+open MiniFun
+open Lexing
+
+(* -------------------------------------------------------------------------- *)
+(*                             Command Arguments                              *)
+
+let () =
+  Clap.description "Interpreter for MiniFun language.";
+
+  let files = Clap.section ~description: "Files to consider." "FILES" in
+  let values = Clap.section ~description: "Input values." "VALUES" in
+
+  let input = Clap.mandatory_string
+      ~description: "Input file."
+      ~placeholder: "FILENAME"
+      ~section: files
+      ~long: "input"
+      ~short: 'i'
+      ()
+  in
+
+  let inputval = Clap.optional_int
+      ~description: "Optional input value to feed to the program. \
+                     If not specified it is read from stdin."
+      ~placeholder: "INT"
+      ~section: values
+      ~long: "value"
+      ~short: 'v'
+      ()
+  in
+
+  let evalb = Clap.flag
+      ~description: "Optional flag for evaluating the generated risc code."
+      ~section: values
+      ~set_long: "eval"
+      ~set_short: 'e'
+      false
+  in
+
+  let output = Clap.optional_string
+      ~description: "Output file. If not specified output is printed on stdout."
+      ~placeholder: "FILENAME"
+      ~section: files
+      ~long: "output"
+      ~long_synonyms: ["out"; "result"]
+      ~short: 'o'
+      ()
+  in
+
+  Clap.close ();
+
+(* -------------------------------------------------------------------------- *)
+(*                                Interpreter                                 *)
+
+  let print_position outx lexbuf =
+    let pos = lexbuf.lex_curr_p in
+    Printf.fprintf outx "Encountered \"%s\" at %s:%d:%d"
+      (Lexing.lexeme lexbuf) pos.pos_fname
+      pos.pos_lnum (pos.pos_cnum - pos.pos_bol + 1)
+  in
+
+  let interpret_file inch (inval: int) outch =
+    let lexbuf = Lexing.from_channel inch in
+    let program =
+      try Parser.prg Lexer.read lexbuf with
+      | Lexer.LexingError msg ->
+        Printf.fprintf stderr "%a: %s\n" print_position lexbuf msg;
+        exit (-1)
+      | Parser.Error ->
+        Printf.fprintf stderr "%a: syntax error\n" print_position lexbuf;
+        exit (-1)
+    in
+    let ty_program =
+      match TypeChecker.typecheck_polymorphic_unbound program with
+      | Ok ty -> ty
+      | Error (`AbsentAssignment msg)
+      | Error (`WrongTypeSpecification msg)
+      | Error (`RecursionNotImplemented msg)
+      | Error (`WrongType msg) ->
+        Printf.fprintf stderr "%s\n" msg;
+        exit (-1)
+    in
+    let return_value =
+      if evalb then
+        match Semantics.reduce program inval with
+          Ok o -> Some o
+        | Error (`AbsentAssignment msg)
+        | Error (`DivisionByZero msg)
+        | Error (`WrongType msg) ->
+          Printf.fprintf stderr "%s\n" msg;
+          exit (-1)
+      else
+        None
+    in
+
+    Printf.fprintf outch "Type of the program: %s\n" (Types.pp_type_f ty_program);
+    match return_value with
+    | Some v -> Printf.fprintf outch "%d\n" v
+    | None -> ()
+  in
+
+
+  let inx = In_channel.open_text input in
+  let outx = match output with
+      None -> stdout
+    | Some f -> Out_channel.open_text f
+  in
+
+  let inputval = match inputval with
+      None -> (
+        Printf.fprintf stdout "Provide the input: ";
+        read_int ()
+      )
+    | Some o -> o
+  in
+  interpret_file inx inputval outx;
+
+  Out_channel.close outx

lib/miniFun/Lexer.mll

@@ -56,6 +56,7 @@ rule read = parse
   | "+"             {PLUS}
   | ","             {COMMA}
   | "-"             {MINUS}
+  | "?"             {QUESTIONMARK}
   | "->"            {TYPEFUNCTION}
   | "/"             {DIVISION}
   | ":"             {COLUMN}

lib/miniFun/Parser.mly

@@ -13,7 +13,7 @@
 %token <int> INT
 %token COMMA COLUMN LEFTPAR RIGHTPAR CMPLESS CMPGREATER PLUS MINUS TIMES
 %token DIVISION MODULO POWER ASSIGNMENT BAND BOR CMP CMPLESSEQ CMPGREATEREQ
-%token FIRST SECOND
+%token FIRST SECOND QUESTIONMARK
 %token EOF
 
 %type <t_exp> prg
@@ -90,6 +90,7 @@ texp:
 typeexp:
   | TYPEINT                               {IntegerType}
   | TYPEBOOL                              {BooleanType}
+  | QUESTIONMARK                          {UnknownType}
   | v = delimited(LEFTPAR, typeexp, RIGHTPAR)
                                           {v}
   | a = typeexp; COMMA; b = typeexp       {TupleType (a, b)}

lib/miniFun/TypeChecker.ml

@@ -5,53 +5,265 @@ Random.self_init ()
 
 let (let*) = Result.bind
 
-let evaluate_type_polimorphic (_program: t_exp) (_context: typingshape) : (typingshape, error) result =
-  failwith "Not implemented"
-  (* match program with *)
-  (*   Integer _ -> Ok (VariableMap.empty, IntegerType) *)
-  (* | Boolean _ -> Ok (VariableMap.empty, BooleanType) *)
-  (* | Variable x -> ( *)
-  (*     match (VariableMap.find_opt x (fst context)) with *)
-  (*       (None) -> ( *)
-  (*         let u = PolimorphicType (Utility.fromIntToString !globalIdentifier) in *)
-  (*         globalIdentifier := !globalIdentifier + 1; *)
-  (*         Ok (VariableMap.singleton x u, u) *)
-  (*       ) *)
-  (*     | (Some u) -> Ok (VariableMap.singleton x u, u) *)
-  (*   ) *)
-  (* | Function (xs, typef, fbody) -> failwith "Not Implemented" *)
-  (* | Application (f, xs) -> failwith "Not Implemented" *)
-  (* | Plus (x, y) *)
-  (* | Minus (x, y) *)
-  (* | Times (x, y) *)
-  (* | Division (x, y) *)
-  (* | Modulo (x, y) *)
-  (* | Power (x, y) -> ( *)
-  (*     let* partialResx = evaluate_type x context in *)
-  (*     let* partialResy = evaluate_type y context in *)
-  (*     match (partialResx, partialResy) with *)
-  (*       ((conx, IntegerType), (cony, IntegerType)) -> *)
-  (*       Ok (VariableMap.union (fun _ x _ -> Some x) conx cony, *)
-  (*           FunctionType ([IntegerType; IntegerType], IntegerType)) *)
-  (*     | ((conx, PolimorphicType xv), (cony, IntegerType)) -> *)
-  (*       Ok (unify ) *)
-  (*     | ((_conx, IntegerType), (_cony, PolimorphicType _yv)) *)
-  (*     | ((_conx, PolimorphicType _xv), (_cony, PolimorphicType _yv)) -> failwith "ads" *)
-  (*     | (_, _) -> Error (`WrongType "The arguments are of the wrong type") *)
-  (*   ) *)
-  (* | PowerMod (x, y, z) -> failwith "Not Implemented" *)
-  (* | Rand (x) -> failwith "Not Implemented" *)
-  (* | BAnd (x, y) *)
-  (* | BOr (x, y) -> failwith "Not Implemented" *)
-  (* | BNot (x) -> failwith "Not Implemented" *)
-  (* | Cmp (x, y) *)
-  (* | CmpLess (x, y) *)
-  (* | CmpLessEq (x, y) *)
-  (* | CmpGreater (x, y) *)
-  (* | CmpGreaterEq (x, y) -> failwith "Not Implemented" *)
-  (* | IfThenElse (guard, if_exp, else_exp) -> failwith "Not Implemented" *)
-  (* | LetIn (x, xval, rest) -> failwith "Not Implemented" *)
-  (* | LetFun (f, xs, typef, fbody, rest) -> failwith "Not Implemented" *)
+(* -------------------------------------------------------------------------- *)
+(*                         polimporphic type checking                         *)
+(* -------------------------------------------------------------------------- *)
+
+let global_type_id = ref 0
+
+let new_global_id () =
+  let id = !global_type_id in
+  incr global_type_id;
+  id
+
+
+let rec unify type_a type_b =
+  if type_a == type_b then Ok () else
+    match (type_a, type_b) with
+    | IntegerTypeP, IntegerTypeP
+    | BooleanTypeP, BooleanTypeP ->
+      Ok ()
+
+    | TupleTypeP (a1, a2), TupleTypeP (b1, b2)
+    | ApplicationP (a1, a2), ApplicationP (b1, b2)
+    | FunctionTypeP (a1, a2), FunctionTypeP (b1, b2) ->
+      let* _ = unify a1 b1 in
+      unify a2 b2
+
+    | VariableTypeP ({contents = Link a1}),
+      VariableTypeP ({contents = Link b1}) ->
+      unify a1 b1
+
+    | VariableTypeP ({contents = Link ty_link}), ty_rest
+    | ty_rest, VariableTypeP ({contents = Link ty_link}) ->
+      unify ty_rest ty_link
+
+    | VariableTypeP ({contents = Unbound (a1, _)}),
+      VariableTypeP ({contents = Unbound (b1, _)})
+      when a1 = b1 ->
+      (* should never happen *)
+      Error (`WrongType "Only a single instance of a type should be available.")
+
+    | type_ab, VariableTypeP ({contents = Unbound (_id, _level)} as tvar)
+    | VariableTypeP ({contents = Unbound (_id, _level)} as tvar), type_ab ->
+      tvar := Link type_ab;
+      Ok ()
+
+    | _, _ ->
+      Error (`WrongType "Cannot unify types.")
+
+let rec unifyable type_a type_b =
+  if type_a == type_b then Ok () else
+    match (type_a, type_b) with
+    | IntegerTypeP, IntegerTypeP
+    | BooleanTypeP, BooleanTypeP ->
+      Ok ()
+
+    | TupleTypeP (a1, a2), TupleTypeP (b1, b2)
+    | ApplicationP (a1, a2), ApplicationP (b1, b2)
+    | FunctionTypeP (a1, a2), FunctionTypeP (b1, b2) ->
+      let* _ = unifyable a1 b1 in
+      unifyable a2 b2
+
+    | VariableTypeP ({contents = Link a1}),
+      VariableTypeP ({contents = Link b1}) ->
+      unifyable a1 b1
+
+    | VariableTypeP ({contents = Link ty_link}), ty_rest
+    | ty_rest, VariableTypeP ({contents = Link ty_link})
+      when ty_link = ty_rest ->
+      Ok ()
+
+    | VariableTypeP ({contents = Unbound (a1, _)}),
+      VariableTypeP ({contents = Unbound (b1, _)})
+      when a1 = b1 ->
+      Error (`WrongType "Only a single instance of a type should be available.")
+
+    | _type_ab, VariableTypeP ({contents = Unbound (_id, _level)})
+    | VariableTypeP ({contents = Unbound (_id, _level)}), _type_ab ->
+      Ok ()
+
+    | _, _ ->
+      Error (`WrongType "Cannot unify types.")
+
+let rec generalize level ty =
+  match ty with
+  | VariableTypeP {contents = Unbound (id, o_level)} when o_level > level ->
+    VariableTypeP (ref (Generic id))
+  | ApplicationP (ty, ty_arg) ->
+    ApplicationP (generalize level ty, generalize level ty_arg)
+  | FunctionTypeP (ty_arg, ty) ->
+    FunctionTypeP (generalize level ty_arg, generalize level ty)
+  | TupleTypeP (ty1, ty2) ->
+    TupleTypeP (generalize level ty1, generalize level ty2)
+  | VariableTypeP {contents = Link ty} ->
+    generalize level ty
+  | VariableTypeP {contents = Generic _}
+  | VariableTypeP {contents = Unbound _}
+  | IntegerTypeP
+  | BooleanTypeP ->
+    ty
+
+
+let instantiate level ty =
+  let var_map = ref IntegerMap.empty in
+  let rec aux ty =
+    match ty with
+    | IntegerTypeP
+    | BooleanTypeP ->
+      ty
+    | TupleTypeP (ty1, ty2) ->
+      TupleTypeP (aux ty1, aux ty2)
+    | VariableTypeP {contents = Link ty} ->
+      aux ty
+    | VariableTypeP {contents = Generic id} -> (
+      match IntegerMap.find_opt id !var_map with
+      | Some ty -> ty
+      | None ->
+        let var = VariableTypeP (ref (Unbound (new_global_id (), level))) in
+        var_map := IntegerMap.add id var !var_map;
+        var
+    )
+    | VariableTypeP {contents = Unbound _} ->
+      ty
+    | ApplicationP (ty, ty_arg) ->
+      ApplicationP (aux ty, aux ty_arg)
+    | FunctionTypeP (ty_arg, ty) ->
+      FunctionTypeP (aux ty_arg, aux ty)
+  in
+  aux ty
+
+
+let rec evaluate_type_polimorphic program (env: env) level =
+  match program with
+  | Integer _ -> Ok (IntegerTypeP)
+  | Boolean _ -> Ok (BooleanTypeP)
+  | Tuple (a, b) ->
+    let* type_a = evaluate_type_polimorphic a env level in
+    let* type_b = evaluate_type_polimorphic b env level in
+    Ok (TupleTypeP (type_a, type_b))
+  | Variable (x) -> (
+      match VariableMap.find_opt x env with
+      | Some (ty) ->
+        Ok (instantiate level ty)
+      | None ->
+        Error (`AbsentAssignment ("Variable " ^ x ^ " is not assigned."))
+    )
+  | Function (x, _typef, fbody) ->
+    let param_type = VariableTypeP (ref (Unbound (new_global_id (), level))) in
+    let fn_env = VariableMap.add x param_type env in
+    let* body_type = evaluate_type_polimorphic fbody fn_env level in
+    Ok (FunctionTypeP (param_type, body_type))
+  | Application (f, xs) ->
+    let* type_f = evaluate_type_polimorphic f env level in
+    let rec aux =
+      function
+      | FunctionTypeP (type_f_arg, type_f) ->
+        Ok (type_f_arg, type_f)
+      | VariableTypeP {contents = Link ty} ->
+        aux ty
+      | VariableTypeP ({contents = Unbound(_id, level)} as tvar) ->
+        let param_ty = VariableTypeP (ref (Unbound (new_global_id (), level)))
+        in
+        let f_ty = VariableTypeP (ref (Unbound (new_global_id (), level))) in
+        tvar := Link ( FunctionTypeP (param_ty, f_ty) );
+        Ok (param_ty, f_ty)
+      | _ -> Error (`WrongType "Expecting a function to apply.")
+    in
+    let* param_ty, f_ty = aux type_f in
+    let* type_xs = evaluate_type_polimorphic xs env level in
+    let* _ = unify param_ty type_xs in
+    Ok f_ty
+  | Plus (a, b)
+  | Minus (a, b)
+  | Times (a, b)
+  | Division (a, b)
+  | Modulo (a, b)
+  | Power (a, b) ->
+    let* type_a = evaluate_type_polimorphic a env level in
+    let* type_b = evaluate_type_polimorphic b env level in
+    let* _ = unify type_a IntegerTypeP in
+    let* _ = unify type_b IntegerTypeP in
+    Ok (IntegerTypeP)
+  | First a -> (
+      let* type_a = evaluate_type_polimorphic a env level in
+      let* _ = unify type_a
+          (TupleTypeP(VariableTypeP (ref (Unbound (new_global_id (), level))),
+                      VariableTypeP (ref (Unbound (new_global_id (), level)))))
+      in
+      match type_a with
+      | TupleTypeP (ty_a, _)
+      | VariableTypeP {contents = Link TupleTypeP (ty_a, _)} -> Ok ty_a
+      | _ -> Error (`WrongType "Applying First to non tuple type.")
+    )
+  | Second a -> (
+      let* type_a = evaluate_type_polimorphic a env level in
+      let* _ = unify type_a
+          (TupleTypeP(VariableTypeP (ref (Unbound (new_global_id (), level))),
+                      VariableTypeP (ref (Unbound (new_global_id (), level)))))
+      in
+      match type_a with
+      | TupleTypeP (_, ty_a)
+      | VariableTypeP {contents = Link TupleTypeP (_, ty_a)} -> Ok ty_a
+      | _ -> Error (`WrongType "Applying Second to non tuple type.")
+    )
+  | PowerMod (x, y, z) ->
+    let* type_x = evaluate_type_polimorphic x env level in
+    let* type_y = evaluate_type_polimorphic y env level in
+    let* type_z = evaluate_type_polimorphic z env level in
+    let* _ = unify type_x IntegerTypeP in
+    let* _ = unify type_y IntegerTypeP in
+    let* _ = unify type_z IntegerTypeP in
+    Ok (IntegerTypeP)
+  | Rand (x) ->
+    let* type_x = evaluate_type_polimorphic x env level in
+    let* _ = unify type_x IntegerTypeP in
+    Ok (IntegerTypeP)
+  | BAnd (a, b)
+  | BOr (a, b) ->
+    let* type_a = evaluate_type_polimorphic a env level in
+    let* type_b = evaluate_type_polimorphic b env level in
+    let* _ = unify type_a BooleanTypeP in
+    let* _ = unify type_b BooleanTypeP in
+    Ok (BooleanTypeP)
+  | BNot (x) ->
+    let* type_x = evaluate_type_polimorphic x env level in
+    let* _ = unify type_x BooleanTypeP in
+    Ok (BooleanTypeP)
+  | Cmp (a, b)
+  | CmpLess (a, b)
+  | CmpLessEq (a, b)
+  | CmpGreater (a, b)
+  | CmpGreaterEq (a, b) ->
+    let* type_a = evaluate_type_polimorphic a env level in
+    let* type_b = evaluate_type_polimorphic b env level in
+    let* _ = unify type_a IntegerTypeP in
+    let* _ = unify type_b IntegerTypeP in
+    Ok (BooleanTypeP)
+  | IfThenElse (guard, if_exp, else_exp) ->
+    let* type_guard = evaluate_type_polimorphic guard env level in
+    let* type_if_exp = evaluate_type_polimorphic if_exp env level in
+    let* type_else_exp = evaluate_type_polimorphic else_exp env level in
+    let* _ = unify type_guard BooleanTypeP in
+    let* _ = unify type_if_exp type_else_exp in
+    Ok (type_if_exp)
+  | LetIn (x, xval, rest) ->
+    let* var_ty = evaluate_type_polimorphic xval env (level + 1) in
+    let generalized_ty = generalize level var_ty in
+    evaluate_type_polimorphic rest (VariableMap.add x generalized_ty env) level
+  | LetFun (f, xs, _typef, fbody, rest) ->
+    let* _ = Error (`RecursionNotImplemented "Let Rec is not implemented.") in
+    let tmp_type_f = VariableTypeP (ref (Unbound (new_global_id (), level))) in
+    let new_env = VariableMap.add f tmp_type_f env in
+    let param_type = VariableTypeP (ref (Unbound (new_global_id (), level))) in
+    let fn_env = VariableMap.add xs param_type new_env in
+    let* body_type = evaluate_type_polimorphic fbody fn_env level in
+    let* _ = unify tmp_type_f body_type in
+    evaluate_type_polimorphic rest (VariableMap.add f tmp_type_f env) level
+
+
+(* -------------------------------------------------------------------------- *)
+
 
 let rec evaluate_type (program: t_exp) (context: ftype VariableMap.t) :
   (ftype, [> typechecking_error]) result =
@@ -200,10 +412,26 @@ let rec evaluate_type (program: t_exp) (context: ftype VariableMap.t) :
     | _ -> Error (`WrongTypeSpecification
                     "Specification of function is not a function type.")
 
+
 let typecheck (program: t_exp) : (ftype, [> typechecking_error]) result =
   let* typeprogram = evaluate_type program VariableMap.empty in
   match typeprogram with
-    FunctionType (IntegerType, IntegerType) -> (
-      Ok (typeprogram)
-    )
+    FunctionType (IntegerType, IntegerType) -> Ok (typeprogram)
   | _ -> Error (`WrongType "Program is not a function from int to int.")
+
+
+let typecheck_polymorphic (program: t_exp)
+  : (type_f, [> polytypechecking_error]) result =
+  global_type_id := 0;
+  let* type_program = evaluate_type_polimorphic program VariableMap.empty 0 in
+  let* _ = unifyable type_program (FunctionTypeP (IntegerTypeP, IntegerTypeP))
+  in
+  let generalized_ty = generalize (-1) type_program in
+  Ok (generalized_ty)
+
+let typecheck_polymorphic_unbound (program: t_exp)
+  : (type_f, [> polytypechecking_error]) result =
+  global_type_id := 0;
+  let* type_program = evaluate_type_polimorphic program VariableMap.empty 0 in
+  let generalized_ty = generalize (-1) type_program in
+  Ok (generalized_ty)

lib/miniFun/TypeChecker.mli

@@ -1 +1,5 @@
-val typecheck : Types.t_exp -> (Types.ftype, [> Types.typechecking_error]) result
+val typecheck                     : Types.t_exp -> (Types.ftype,  [> Types.typechecking_error]) result
+
+val typecheck_polymorphic         : Types.t_exp -> (Types.type_f, [> Types.polytypechecking_error]) result
+
+val typecheck_polymorphic_unbound : Types.t_exp -> (Types.type_f, [> Types.polytypechecking_error]) result

lib/miniFun/Types.ml

@@ -5,18 +5,80 @@ let globalIdentifier = ref 1
 module VariableMap = Map.Make(String)
 module VariableSet = Set.Make(String)
 
-type ftype =
+(* -------------------------------------------------------------------------- *)
+(*                      polimporphic type checking types                      *)
+(* -------------------------------------------------------------------------- *)
+
+type id = int
+type level = int
+
+type type_f =
+    IntegerTypeP
+  | BooleanTypeP
+  | TupleTypeP of type_f * type_f
+  | VariableTypeP of variable_type ref
+  | FunctionTypeP of type_f * type_f
+  | ApplicationP of type_f * type_f
+and variable_type =
+    Unbound of id * level
+  | Link of type_f
+  | Generic of id
+
+type env = type_f VariableMap.t
+module IntegerMap = Map.Make(Int)
+
+let pp_type_f (ty: type_f) : string =
+  let id_name_map = ref IntegerMap.empty in
+  let count = ref 0 in
+  let next_name () =
+    let i = !count in
+    incr count;
+    Utility.from_int_to_string i
+  in
+  let rec aux is_simple ty =
+    match ty with
+    | IntegerTypeP -> "Int"
+    | BooleanTypeP -> "Bool"
+    | TupleTypeP (ty1, ty2) ->
+      "(" ^ aux is_simple ty1 ^ ", " ^ aux is_simple ty2 ^ ")"
+    | ApplicationP (ty, ty_arg) ->
+      aux true ty ^ "(" ^ aux false ty_arg ^ ")"
+    | FunctionTypeP (ty_arg, ty) ->
+      let ty_arg_str = aux true ty_arg in
+      let ty_str = aux false ty in
+      let str = ty_arg_str ^ " -> " ^ ty_str in
+      if is_simple then "(" ^ str ^ ")" else str
+    | VariableTypeP {contents = Generic id} -> (
+        match IntegerMap.find_opt id !id_name_map with
+        | Some a -> a
+        | None ->
+          let name = next_name () in
+          id_name_map := IntegerMap.add id name !id_name_map;
+          name
+      )
+    | VariableTypeP {contents = Unbound (id, _)} ->
+      "_" ^ string_of_int id
+    | VariableTypeP {contents = Link ty} ->
+      aux is_simple ty
+  in
+  let ty_str = aux false ty in
+  if !count > 0 then
+    let var_names =
+      IntegerMap.fold (fun _ value acc -> value :: acc) !id_name_map []
+    in
+    "∀ " ^ (String.concat " " (List.sort String.compare var_names))
+    ^ ", " ^ ty_str
+  else
+    ty_str
+
+(* -------------------------------------------------------------------------- *)
+
+type ftype = (* type used for specification *)
     IntegerType
   | BooleanType
+  | UnknownType
   | TupleType of ftype * ftype
-  | PolimorphicType of string
   | FunctionType of ftype * ftype
-type fsubstitution = (* goes from polimorphic types to types *)
-  ftype VariableMap.t
-type fenvironment = (* goes from variables to types *)
-  ftype VariableMap.t
-type typingshape = (* tuple of a simple type environment and a simple type *)
-  fenvironment * ftype
 
 type t_exp =
     Integer of int                                  (* x := a *)
@@ -75,6 +137,12 @@ type typechecking_error = [
   | `WrongTypeSpecification of string
 ]
 
+type polytypechecking_error = [
+  | typechecking_error
+  | `RecursionNotImplemented of string
+]
+
+
 type error = [
   | base_error
   | `DivisionByZero of string

lib/miniFun/Types.mli

@@ -5,73 +5,68 @@ val globalIdentifier : int ref
 module VariableMap : Map.S with type key = variable
 module VariableSet : Set.S with type elt = string
 
-type ftype =
+(* -------------------------------------------------------------------------- *)
+(*                      polimporphic type checking types                      *)
+(* -------------------------------------------------------------------------- *)
+
+type id = int
+type level = int
+
+type type_f =
+    IntegerTypeP
+  | BooleanTypeP
+  | TupleTypeP of type_f * type_f
+  | VariableTypeP of variable_type ref
+  | FunctionTypeP of type_f * type_f
+  | ApplicationP of type_f * type_f
+and variable_type =
+    Unbound of id * level
+  | Link of type_f
+  | Generic of id
+
+type env = type_f VariableMap.t
+module IntegerMap : Map.S with type key = int
+
+val pp_type_f : type_f -> string
+
+(* -------------------------------------------------------------------------- *)
+
+type ftype = (* type used for specification *)
     IntegerType
   | BooleanType
+  | UnknownType
   | TupleType of ftype * ftype
-  | PolimorphicType of variable
   | FunctionType of ftype * ftype
-type fsubstitution = (* goes from polimorphic types to types *)
-  ftype VariableMap.t
-type fenvironment = (* goes from variables to types *)
-  ftype VariableMap.t
-type typingshape = (* tuple of a simple type environment and a simple type *)
-  fenvironment * ftype
-
-type intermediaryType =
-    IInteger
-  | IBoolean
-  | IVariable of variable
-  | IFunction of variable list * ftype list * intermediaryType
-  | IApplication of intermediaryType * intermediaryType list
-  | IPlus of intermediaryType * intermediaryType
-  | IMinus of intermediaryType * intermediaryType
-  | ITimes of intermediaryType * intermediaryType
-  | IDivision of intermediaryType * intermediaryType
-  | IModulo of intermediaryType * intermediaryType
-  | IPower of intermediaryType * intermediaryType
-  | IPowerMod of intermediaryType * intermediaryType * intermediaryType
-  | IRand of intermediaryType
-  | IBAnd of intermediaryType * intermediaryType
-  | IBOr of intermediaryType * intermediaryType
-  | IBNot of intermediaryType
-  | ICmp of intermediaryType * intermediaryType
-  | ICmpLess of intermediaryType * intermediaryType
-  | ICmpLessEq of intermediaryType * intermediaryType
-  | ICmpGreater of intermediaryType * intermediaryType
-  | ICmpGreaterEq of intermediaryType * intermediaryType
-  | IIfThenElse of intermediaryType * intermediaryType * intermediaryType
-  | ILetIn of variable * ftype * intermediaryType * intermediaryType
-  | ILetFun of variable * ftype * variable list * ftype list * intermediaryType * intermediaryType
 
 type t_exp =
-    Integer of int                                             (* x := a *)
-  | Boolean of bool                                            (* v *)
-  | Variable of variable                                       (* x *)
-  | Tuple of t_exp * t_exp                                     (* (a, b) *)
-  | Function of variable * ftype * t_exp                       (* lambda x: t. x *)
-  | Application of t_exp * t_exp                               (* x x *)
-  | Plus of t_exp * t_exp                                      (* x + x *)
-  | Minus of t_exp * t_exp                                     (* x - x *)
-  | Times of t_exp * t_exp                                     (* x * x *)
-  | Division of t_exp * t_exp                                  (* x / x *)
-  | Modulo of t_exp * t_exp                                    (* x % x *)
-  | Power of t_exp * t_exp                                     (* x ^ x *)
-  | PowerMod of t_exp * t_exp * t_exp                          (* (x ^ x) % x *)
-  | Rand of t_exp                                              (* rand(0, x) *)
-  | BAnd of t_exp * t_exp                                      (* x && x *)
-  | BOr of t_exp * t_exp                                       (* x || x *)
-  | BNot of t_exp                                              (* not x *)
-  | First of t_exp                                             (* fst x *)
-  | Second of t_exp                                            (* scn x *)
-  | Cmp of t_exp * t_exp                                       (* x == x *)
-  | CmpLess of t_exp * t_exp                                   (* x < x *)
-  | CmpLessEq of t_exp * t_exp                                 (* x <= x *)
-  | CmpGreater of t_exp * t_exp                                (* x > x *)
-  | CmpGreaterEq of t_exp * t_exp                              (* x >= x *)
-  | IfThenElse of t_exp * t_exp * t_exp                        (* if b then c else c *)
-  | LetIn of variable * t_exp * t_exp                          (* let x = x in x *)
-  | LetFun of variable * variable * ftype * t_exp * t_exp      (* let rec x. y: t. x in x*)
+    Integer of int                                  (* x := a *)
+  | Boolean of bool                                 (* v *)
+  | Variable of variable                            (* x *)
+  | Tuple of t_exp * t_exp                          (* (a, b) *)
+  | Function of variable * ftype * t_exp            (* lambda x: t. x *)
+  | Application of t_exp * t_exp                    (* x x *)
+  | Plus of t_exp * t_exp                           (* x + x *)
+  | Minus of t_exp * t_exp                          (* x - x *)
+  | Times of t_exp * t_exp                          (* x * x *)
+  | Division of t_exp * t_exp                       (* x / x *)
+  | Modulo of t_exp * t_exp                         (* x % x *)
+  | Power of t_exp * t_exp                          (* x ^ x *)
+  | PowerMod of t_exp * t_exp * t_exp               (* (x ^ x) % x *)
+  | Rand of t_exp                                   (* rand(0, x) *)
+  | BAnd of t_exp * t_exp                           (* x && x *)
+  | BOr of t_exp * t_exp                            (* x || x *)
+  | BNot of t_exp                                   (* not x *)
+  | First of t_exp                                  (* fst x *)
+  | Second of t_exp                                 (* scn x *)
+  | Cmp of t_exp * t_exp                            (* x == x *)
+  | CmpLess of t_exp * t_exp                        (* x < x *)
+  | CmpLessEq of t_exp * t_exp                      (* x <= x *)
+  | CmpGreater of t_exp * t_exp                     (* x > x *)
+  | CmpGreaterEq of t_exp * t_exp                   (* x >= x *)
+  | IfThenElse of t_exp * t_exp * t_exp             (* if b then c else c *)
+  | LetIn of variable * t_exp * t_exp               (* let x = x in x *)
+  | LetFun of variable * variable * ftype * t_exp * t_exp
+                                                    (* let rec x. y: t. x in x*)
 
 type permitted_values =
     IntegerPermitted  of int
@@ -100,6 +95,11 @@ type typechecking_error = [
   | `WrongTypeSpecification of string
 ]
 
+type polytypechecking_error = [
+  | typechecking_error
+  | `RecursionNotImplemented of string
+]
+
 type error = [
   | base_error
   | `DivisionByZero of string

lib/miniFun/dune

@@ -5,7 +5,7 @@
  (explain true)
  (infer true)
  (flags --dump --table)
- )
+)
 
 (library
  (name miniFun)

lib/miniImp/dune

@@ -5,7 +5,7 @@
  (explain true)
  (infer true)
  (flags --dump --table)
- )
+)
 
 (library
  (name miniImp)

lib/utility/utility.ml

@@ -15,13 +15,13 @@ let rec powmod a d = function
 let alphabet = "abcdefghijklmnopqrstuvwxyz"
 let base = 26
 
-let rec fromIntToString (x: int) : string =
+let rec from_int_to_string (x: int) : string =
   if x < 0 then
     ""
   else if x < base then
     String.get alphabet x |> String.make 1
   else
-    (fromIntToString (x/base - 1)) ^ (String.get alphabet (x mod base) |> String.make 1)
+    (from_int_to_string (x/base - 1)) ^ (String.get alphabet (x mod base) |> String.make 1)
 
 let int_and a b =
   match (a>0, b>0) with
@@ -169,4 +169,3 @@ let rec combine_twice la lb =
   | [a], [b] -> [a, b]
   | a::la, b::lb -> (a, b) :: (combine_twice la lb)
   | _ -> []
->>>>>>> cfg

lib/utility/utility.mli

@@ -1,7 +1,7 @@
 val pow :    int -> int -> int
 val powmod : int -> int -> int -> int
 
-val fromIntToString : int -> string
+val from_int_to_string : int -> string
 
 val int_and :     int -> int -> int
 val int_or :      int -> int -> int

report/document.bib

@@ -0,0 +1,19 @@
+@article{MILNER,
+  title = {A theory of type polymorphism in programming},
+  journal = {Journal of Computer and System Sciences},
+  volume = {17},
+  number = {3},
+  pages = {348-375},
+  year = {1978},
+  issn = {0022-0000},
+  doi = {https://doi.org/10.1016/0022-0000(78)90014-4},
+  url = {www.sciencedirect.com/science/article/pii/0022000078900144},
+  author = {Robin Milner},
+}
+
+@inproceedings{REMY,
+  title={Extension of ML type system with a sorted equation theory on types},
+  author={Didier R{\'e}my},
+  year={1992},
+  url={https://api.semanticscholar.org/CorpusID:117549268}
+}

report/document.tex

@@ -153,7 +153,7 @@
 \newcommand{\defeq}{\vcentcolon=}
 
 \lstdefinelanguage{miniimp}{
-  keywords={if, then, else, skip, while, do, for, rand},
+  keywords={if, then, else, skip, while, do, for, rand, let},
   keywordstyle=\color{blue}\bfseries,
   identifierstyle=\color{black},
   sensitive=false,
@@ -202,6 +202,8 @@
 
 \input{report}
 
+\printbibliography{}
+
 \end{document}
 
 %% - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - %%

report/report.tex

@@ -408,7 +408,7 @@ output := y;
 \end{section}
 
 \begin{section}{Target Code Generation}
-  In the files \href{../lib/miniImp/reduceRegisters.ml}{reduceRegisters.ml} and \href{../lib/miniImp/reduceRegisters.mli}{reduceRegisters.mli} the function \texttt{reduceregisters} reduces the number of used registers by counting the syntactic occurrence of each variable and partitioning the set keeping the most used as registers. All registers are either renamed or put into memory. It is allowed for the input or output registers to be put in memory, in the latter case some code is added at the end of the program to retrieve the value and put into a register (in particular register \texttt{2}).
+  In the files \href{../lib/miniImp/reduceRegisters.ml}{reduceRegisters.ml} and \href{../lib/miniImp/reduceRegisters.mli}{reduceRegisters.mli} the function \texttt{reduce_registers} reduces the number of used registers by counting the syntactic occurrence of each variable and partitioning the set keeping the most used as registers. All registers are either renamed or put into memory. It is allowed for the input or output registers to be put in memory, in the latter case some code is added at the end of the program to retrieve the value and put into a register (in particular register \texttt{2}).
 
   \begin{subsection}{MiniImp to MiniRISC compiler}
     The file \href{../bin/miniImpInterpreterReg.ml}{miniImpInterpreterReg.ml} compiles from MiniImp to MiniRISC or execute the MiniRISC code. It uses the package \href{https://opam.ocaml.org/packages/clap/}{Clap} to parse command line arguments and generate help pages.
@@ -426,6 +426,39 @@ output := y;
 
   To see a list of all options run \texttt{dune exec <interpreter> {-}{-} -h}. A binary version of the executables can also be found in the build directory: \href{./_build/default/bin/}{./\_build/default/bin/}.
 \end{section}
+
+
+\begin{section}{Addendum: Algorithm W}
+  Added since the last submission a simplified version of the Algorithm W from {\bf A Theory of Type Polymorphism in Programming}\cite{MILNER} for the miniFun language. The implementation uses levels instead of prefixes as described in {\bf Extension of ML type system with a sorted equation theory on types}\cite{REMY} and \href{https://okmij.org/ftp/ML/generalization.html}{okmij.org/ftp/ML/generalization.html}, but does not contain a fixed point operator. Meaning \texttt{let rec} is not implemented. But the remaining grammar is fully polimorphically typable.
+  An interpreter that outputs the type of the input program is provided as \href{../bin/miniFunPolyInterpreter.ml}{miniFunPolyInterpreter.ml}. The interpreter admits program that are not functions from integers to integers like with the other interpreter, so the evaluation of the program with input is disabled by default. Otherwise the only possible types of programs would be \(\texttt{Int} \to \texttt{Int}\), \(\forall \texttt{a}, \texttt{a} \to \texttt{Int}\) and \(\forall \texttt{a}, \texttt{a} \to \texttt{a}\) since they can be all unified with \(\texttt{Int} \to \texttt{Int}\).
+  In addition the character \texttt{?} is mapped to the new type \texttt{Unknown}. The new type is not used by the program and any type specification is ignored. The \texttt{?} symbol is just a useful shorthand.
+
+
+  Some examples:
+\begin{lstlisting}
+let f =
+  \z: ? =>
+    \y: ? =>
+      \x: ? =>
+        if x < 0 then y x else z x
+in f
+\end{lstlisting}
+  
+  is correctly evaluated as having the type \( \forall \texttt{a}, (\texttt{Int} \to \texttt{a}) \to (\texttt{Int} \to \texttt{a}) \to \texttt{Int} \to \texttt{a} \).
+
+  \begin{lstlisting}
+let f =
+  \z: ? =>
+    \y: ? =>
+      \x: ? =>
+        if x < 0 then y x else z x
+in
+f (\x: ? => \y: ? => \z: ? => if fst y then snd y else snd z)
+\end{lstlisting}
+  
+is correctly evaluated as having the type \( \forall \texttt{a}\ \texttt{b}, (\texttt{Int} \to (\texttt{Bool}, \texttt{a}) \to (\texttt{b}, \texttt{a}) \to \texttt{a}) \to \texttt{Int} \to (\texttt{Bool}, \texttt{a}) \to (\texttt{b}, \texttt{a}) \to \texttt{a} \).
+\end{section}
+
 %%% Local Variables:
 %%% TeX-command-extra-options: "-shell-escape"
 %%% TeX-master: "document.tex"

seminar/document.tex

@@ -0,0 +1,213 @@
+\documentclass[
+    11pt,
+    %draft
+]{beamer}
+ 
+\usetheme{Antibes} % or Malmoe -> more somber
+
+%% - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - %%
+%%                               Load Packages                               %%
+%% - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - %%
+
+\usepackage[utf8]{inputenc} %% use UTF-8, maybe not needed since 2018
+\usepackage[main=english]{babel} %% language
+
+
+\usepackage[
+  backend=biber,
+  style=numeric,
+  sorting=ynt
+]{biblatex} %% for citations
+\addbibresource{document.bib}
+
+\usepackage{import} %% specify path for import
+
+%% math packages
+\usepackage{graphicx} %% for pictures
+\usepackage{float}
+\usepackage{amssymb} %% math symbols
+\usepackage{amsmath} %% math matrix etc
+\usepackage{minted} %% code block
+\usepackage{tabularray} %% better tables
+\usepackage{booktabs} %% rules for tables
+\usepackage{mathrsfs}
+\usepackage{mathtools}
+\usepackage{algorithm} %% for algorithms
+\usepackage{algpseudocode} %% loads algorithmicx
+\usepackage{amsthm}
+\usepackage{thmtools} %% theorems
+\usepackage{cmll}
+\usepackage{leftindex}
+\usepackage{semantic} %% semantics
+\usepackage{formal-grammar} %% BNF
+
+\usepackage{csquotes} %% correct language also for citations
+
+%% plot packages
+\usepackage{pgfplots} %% plots used with \begin{tikzpicture}
+\usepackage{tikz} %% for pictures
+\usetikzlibrary{trees,chains,shadows.blur,fit,arrows.meta,positioning}
+\pgfplotsset{width=10cm,compat=newest}
+
+%% design packages
+\usepackage{color}
+\usepackage{xcolor,colortbl} % xcolor for defining colors, colortbl for table colors
+\usepackage{makecell} %% for multiple lines in cell of table
+\usepackage{cancel}
+\usepackage{pgfornament} %% ornaments
+
+
+
+%% - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - %%
+%%                       Configuration of the packages                       %%
+%% - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - %%
+
+\linespread{1}
+\raggedbottom %% spaces if page is empty % chktex 1
+
+%% set max table of contents recursion to subsection (3->subsubsecition)
+\setcounter{tocdepth}{3}
+\setcounter{secnumdepth}{3}
+
+%% use bar instead of arrow for vectors
+\renewcommand{\vec}[1]{\bar{#1}}
+%% easy norm
+\newcommand{\norm}[1]{\left\lvert#1\right\rvert}
+
+% argmin and argmax
+\DeclareMathOperator*{\argmax}{argmax}
+\DeclareMathOperator*{\argmin}{argmin}
+
+% %% itemize use less vertical space (use olditemize for default behaviour)
+% \let\olditemize=\itemize%% old itemize
+% \let\endolditemize=\enditemize%% old end itemize
+% \renewenvironment{itemize}{\olditemize\itemsep+0.1em}{\endolditemize}
+
+%% items in itemize emph+box
+%% usage: \ieb{Class:} for simple item
+%%        \ieb[4cm]{Class:} for specific size of box
+\newcommand{\ieb}[2][2cm]{
+        \makebox[#1][l]{\emph{#2}}
+} %% TODO: replace with description environment (? maybe)
+
+% section not in table of contents
+\newcommand{\hiddensection}[1]{
+  \stepcounter{section}
+  \section*{{#1}}
+}
+
+\newcommand{\hiddensubsection}[1]{
+  \stepcounter{subsection}
+  \subsection*{{#1}}
+}
+
+% less vertical space around align & align*
+\newcommand{\zerodisplayskips}{
+  \setlength{\abovedisplayskip}{0pt}
+  \setlength{\belowdisplayskip}{0pt}
+  \setlength{\abovedisplayshortskip}{0pt}
+  \setlength{\belowdisplayshortskip}{0pt}
+}
+
+% make dotfill use all the space available
+\renewcommand{\dotfill}{
+  \leavevmode\cleaders\hbox to 1.00em{\hss .\hss }\hfill\kern0pt } % chktex 1 chktex 26
+
+\setlength{\fboxsep}{-\fboxrule} % for debugging
+
+
+%% PACKAGE algorithm
+\floatname{algorithm}{Algorithm}
+
+
+%% PACKAGE tabularray
+\UseTblrLibrary{amsmath}
+\UseTblrLibrary{booktabs}
+
+%% PACKAGE color
+\definecolor{red}{rgb}{1, 0.1, 0.1}
+\definecolor{lightgreen}{rgb}{0.55, 0.87, 0.47}
+\definecolor{gray}{rgb}{0.4, 0.4, 0.4}
+\definecolor{blue}{rgb}{0.2, 0.2, 0.675}
+\newcommand{\lgt}{\cellcolor{lightgreen}} %% light green in tables
+\newcommand{\graytext}{\textcolor{gray}} %% gray text
+\newcommand{\rd}{\textcolor{red}} %% red text
+\newcommand{\bluetext}{\textcolor{blue}} %% red text
+
+%% PACKAGE minipage
+\newcommand{\thend}[1]{\begin{center}
+  \begin{minipage}[c][1em][c]{#1}
+    \dotfill{}
+  \end{minipage}
+\end{center}}
+
+
+%% PACKAGE thmtools
+\declaretheoremstyle[
+ headfont=\normalfont\bfseries,
+ notefont=\mdseries,
+ bodyfont=\normalfont,
+ qed=\qedsymbol % chktex 1
+]{steo}
+\declaretheorem[numbered=no, style=steo]{mtheo}
+
+\declaretheoremstyle[
+  headfont=\normalfont\bfseries,
+  notefont=\mdseries,
+  bodyfont=\normalfont,
+]{sdef}
+\declaretheorem[numbered=no, style=sdef]{mdef}
+
+\declaretheoremstyle[
+  spaceabove=-6pt,
+  spacebelow=6pt,
+  headfont=\normalfont\bfseries,
+  bodyfont=\normalfont,
+  postheadspace=1em,
+  qed=$\blacksquare$,
+  headpunct={:}
+]{sprf}
+\declaretheorem[name={Proof}, style=sprf, numbered=no]{mproof}
+
+%% ......................................................................... %%
+%% local changes
+% \setcounter{secnumdepth}{0}
+
+
+%% - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - %%
+
+\title{SEMINAR:\\
+ A Unified View of Modalities in Types Systems}
+\author{Elvis Rossi}
+\institute[DEPARTMENT OF COMPUTER SCIENCE]{Department of Computer Science\\
+  \medskip
+  University of Pisa\\
+  \medskip
+  Master Degree in Computer Science
+}
+\date{\today}
+\logo{\includegraphics[width=1cm]{figures/cherubino.eps}}
+
+%% - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - %%
+
+\begin{document}
+
+\begin{frame}
+  \titlepage % chktex 1
+\end{frame}
+
+\section*{Table of Contents}
+\begin{frame}[allowframebreaks]
+  \frametitle{Table of Contents}
+  \tableofcontents
+\end{frame}
+
+\include{seminar.tex}
+
+\end{document}
+
+%% - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - %%
+
+%%% Local Variables:
+%%% TeX-command-extra-options: "-shell-escape"
+%%% End:

seminar/seminar.tex

@@ -0,0 +1,631 @@
+\AtBeginSection[ ]
+{
+\begin{frame}{Outline}
+    \tableofcontents[currentsection]
+\end{frame}
+}
+
+\begin{section}{Modalities}
+  \begin{frame}{In Philosophy}
+    A modality in philosophy and formally in formal logic/type theory expresses a certain mode (or ``moment'' as in Hegel) of being.
+
+    According to Kant the four “categories” are:
+    \begin{itemize}
+    \item Quantity
+    \item Quality
+    \item Relation
+    \item Modality
+    \end{itemize}
+    and the modalities contain the three pairs of opposites:
+
+    \begin{itemize}
+    \item possibility --- impossibility
+    \item being --- nothing
+    \item necessity --- Zufälligkeit
+    \end{itemize}
+  \end{frame}
+
+  \begin{frame}{In formal logic and type theory}
+    In formal logic and type theory modalities are formalized by modal operators or closure operators
+    \#, that send propositions/types \(X\) to new propositions/types \#\(X\), satisfying some properties.
+    \hspace{1em}\\
+
+    Adding such modalities to propositional logic or similar produces what is called modal logic. Here the most famous modal operators are those meant to formalize necessity (denoted \(\Box\)) and possibility (denoted \(\lozenge\)), which together form S4 modal logic.
+    Similarly, adding modalities more generally to type theory and homotopy type theory yields modal type theory and modal homotopy type theory
+
+    %% modalities are thus qualifiers that apply to types or propositions.
+    %% the paper seeks to provide a generic framework for modalities powerful enough to be instanciated to useful specific application
+    %% and contrained enough to come with a rich meta-theory.
+  \end{frame}
+\end{section}
+
+\AtBeginSection[ ]
+{
+\begin{frame}{Outline}
+    \tableofcontents[currentsection]
+\end{frame}
+}
+
+\begin{section}{Introduction}
+  \begin{frame}{Ringoid of Modalities}
+    %% we begin by presenting the modality structure: a ring-like wich parameterises the calculus \Lambda^p
+    %% three operations are needed: addition, multiplication and meet. and two elements for the ring structure.
+    The modality structure is a ring-like structure, which parameterises the calculus \(\Lambda^p\).
+
+    It is a 6-tuple consisting of a set M, addition (+), multiplication (\(\cdot\)), meet (\(\wedge\)), element 0 and element 1.
+  \end{frame}
+
+  \begin{frame}
+    \begin{itemize}
+    \item<1-> (M, +, 0) forms a commutative monoid (associative and commutative), with 0 as identity
+    \item<2-> (M, \(\cdot\), 1) forms a monoid (associative), with 1 as identity
+    \item<3-> 0 is an absorbing element for multiplication: \( p \cdot 0 = 0 \cdot p = 0 \)
+    \item<4-> (M, \(\wedge\)) forms a semilattice: meet is associative, commutative and idempotent.
+    \item<5-> multiplication distributes over addition: \(p (q + r) = pq + pr\) and \((p+q) r = pr + qr\)
+    \item<5-> multiplication distributes over meet: \(p (q \wedge r) = pq \wedge pr\) and \((p\wedge q) r = pr \wedge qr\)
+    \item<5-> addition distributes over meet: \((p \wedge q) + r = (p + r) \wedge (q + r)\)
+    \end{itemize}
+
+    %% addition is used to combine modalities of two components of a term which are both run,
+    %% for example the function and the argument of an application.
+    %% 0 corresponds to no usage
+
+    %% multiplication arises from function composition and is the principal means
+    %% to combine modalities (qualifying a single type with several modalities);
+    %% its unit (1) corresponds to the identity function, or, more generally,
+    %% a single (non-qualified) use, like a plain variable occurrence.
+
+    %% meet can be used to match modalities between the branches of a conditional, via weakening
+  \end{frame}
+
+  \begin{frame}
+    \begin{definition}[Order]
+      \[(p \leq q) \triangleq (p = p \wedge q)\]
+    \end{definition}
+    %% This is the standard partial order arising from semi-lattices.
+
+    %% Note that addition and multiplication are monotone with respect to (⩽), as a consequence of the
+    %% corresponding distributivity.
+  \end{frame}
+
+  \begin{frame}
+    %% also a context is needed, in order to map variables to the modality expression associated
+    \begin{definition}[Modality context]
+      A modality context (or usage map) is defined as a map from variable names to modality expressions.
+      %% expressions are formed from variables, constants, sums products and meets.
+      %% all variables not specified are mapped to 0
+      %% referred by the symbols \gamma, \delta and \zeta (lowercase greek letters)
+    \end{definition}
+
+    \begin{itemize}
+    \item Every variable in the judgement \(\gamma \Gamma \vdash t : A\) is qualified by a modality.\\
+    \item \(t\) has type \(A\) with unit qualification, in context \(\gamma\Gamma\)\\
+    \item notation: \(\gamma\Gamma, x : \leftindex^{p}A \triangleq (\gamma, x \mapsto p) (\Gamma,x : A)\)
+    \end{itemize}
+  \end{frame}
+
+  \begin{frame}
+    Some properties:
+    %% addition, meet and scaling by q (multipling by q) are lifted to act pointwise on modality contexts:
+    \begin{center}
+      \begin{align*}
+        (\gamma + \delta) (x) &= \gamma(x) + \delta(x),\\
+        (\gamma \wedge \delta) (x) &= \gamma (x) \wedge \delta (x),\\
+        (q \cdot \gamma) (x) &= q \cdot \gamma (x)\\
+      \end{align*}
+    \end{center}
+
+    %% in particular modality contexts form a left module to ringoid M.
+    %% Modules are just generalisations of vector spaces where the scalar q comes from a ring rather than a field.
+  \end{frame}
+
+  \begin{frame}{Predicative Polymorphic Lambda Calculus with Modalities}
+    \(\Lambda^p\) is a functional programming language with:
+    \begin{itemize}
+    \item predicative polymorphism \(\forall \alpha. B\),
+    \item modal function types \(\leftindex^{p}A \to B\),
+    \item modal boxing \(p \langle A \rangle\),
+    \item and modality polymorphism \(\forall m.B\).
+    \end{itemize}
+
+    %% the important construct is the modal boxing operator, that forms a new type: A qualified by modality p
+
+    %% the language lacks recursion on type and term level, but Church encoding can be used represent some inductive data types.
+    %% But we have that it is total and strongly normalising, meaning that it can be used as a consistent logic.
+  \end{frame}
+
+  \begin{frame}{Types}
+    \begin{definition}
+      Types \(A, B, C \in \texttt{Ty}\) are given by the following grammar:
+      \begin{center}
+        \begin{grammar}
+          \firstcase{\text{A,B,C}}{K \gralt{} 1 \gralt{} \alpha}{}
+          \otherform{\forall{} \alpha.A \gralt{} \forall{} m.A}{}
+          \otherform{\vphantom{a}^{p}A \to{} B \gralt{} A + B}{}
+          \otherform{A \times{} B \gralt{} p \langle{} A \rangle{}}{}
+        \end{grammar}
+      \end{center}
+    \end{definition}
+    %% K ranges over a set TyConst of uninterpreted base types, to add to 1, +, \times, \to and p\langle_\rangle
+    %% Boolean type can, for example be encoded as Bool = 1 + 1
+
+    Let Ty\(_0\) denote the set of monomorphic types (monotypes).\\
+    %% types free of polymorphism (dont contain sub-expressions of the form \forall \alpha.B)
+    If \(\alpha\) is restricted to only monotypes, \(\Lambda^p\) becomes predicative.\\
+    %% in particular B[A/\alpha] < \forall \alpha.B is well-founded (where A is a monotype)
+    Let Ty\(_0^0\) denote the set of closed monotypes.
+    %% types that neither contain type quantification nor type variables.
+  \end{frame}
+
+  \begin{frame}
+    %% the key idea is to that modalities operate multiplicatly with respect to the context, and additively over each other.
+    \begin{itemize}
+    \item If \(\gamma \Gamma \vdash A\) then \(p \gamma \Gamma\) is needed to produce \(p \langle A \rangle\).
+    \item If \(\gamma \Gamma \vdash A\) and \(\delta \Gamma \vdash B\), then \((\gamma + \delta)\Gamma\) is needed to produce both \(A\) and \(B\).
+    \end{itemize}
+  \end{frame}
+
+  \begin{frame}
+    %% lets see how functions are encoded:
+    \[\leftindex^{p}A \to B\]
+    %% is the domain of function types quantified with an arbitrary modality expression p.
+    %% ommitted modality implicitly stands for 1
+    \pause\[\leftindex^{1}A \to B\quad = \quad A \to B\quad = \quad A \multimap B\]
+
+    %% we can also apply a modality directly to a type
+    \pause\[\leftindex^{p}A \to B\quad = \quad p\langle A\rangle \to B\]
+    %% both are typing rules for pedagogical purpuses
+  \end{frame}
+
+  \begin{frame}
+    In a language with generalised algebraic data types, \(p\langle A \rangle \)
+    would be defined instead as a data type with constructor of type \[\leftindex^{p}A \to p \langle A \rangle \]
+  \end{frame}
+
+  \begin{frame}\frametitle{Typing rules for \(\Lambda^p\)}
+    %% lets see now how we evaluate the types of the language:
+
+    %% from simply typed lambda calculus rules
+    %% note that in the variable since A is used only once, it is decorated with modality one
+    %% and the rest of the context is not used.
+
+    %% the abstraction rule simply carries the information of the modality
+    \fboxsep=0pt
+    \noindent
+    \begin{minipage}[t]{0.40\linewidth}
+      \begin{center}
+        \bluetext{System F}\\
+        \bluetext{({\it from lambda calculus\/})}
+      \end{center}
+      \footnotesize{
+        \inference[VAR]
+        {}
+        {\Gamma, \graytext{x:}\ A |- \graytext{x:}\ A} % chktex 1
+        \vspace{2em}
+        \inference[ABS]
+        {\Gamma, \graytext{x:}\ A |- \graytext{t:}\ B} % chktex 1
+        {\Gamma |- \lambda x.t: A -> B} % chktex 1
+        \vspace{2em}
+        \inference[APP]
+        {\Gamma |- \graytext{t:}\ A -> B \quad \Gamma |- \graytext{u:}\ A} % chktex 1
+        {\Gamma |- \graytext{t\ u:}\ B} % chktex 1
+      }
+    \end{minipage}
+    \hfill
+    \begin{minipage}[t]{0.55\linewidth}
+      \begin{center}
+        \bluetext{\(\Lambda^p\)}\\
+        \phantom{\bluetext{({\it from lambda calculus\/})}}
+      \end{center}
+      \footnotesize{
+        \inference[VAR]
+        {}
+        {\rd{0}\Gamma, \graytext{x:} \leftindex^{\rd{1}}A |- \graytext{x:}\ A} % chktex 1
+        \vspace{1.9em}
+        \inference[ABS]
+        {\rd{\gamma}\Gamma, \graytext{x:}\leftindex^{\rd{q}} A |- \graytext{t:}\ B} % chktex 1
+        {\rd{\gamma}\Gamma |- \graytext{\lambda \leftindex^{\rd{q}}x.t:} \leftindex^{\rd{q}}A -> B} % chktex 1
+        \vspace{1.5em}
+        \inference[APP]
+        {\rd{\gamma}\Gamma |- \graytext{t:} \leftindex^{\rd{q}} A -> B \quad \rd{\delta} \Gamma |- \graytext{u:}\ A} % chktex 1
+        {\rd{(\gamma + q \delta)}\Gamma |- \graytext{t \leftindex^{\rd{q}} u:}\ B} % chktex 1
+      }
+    \end{minipage}
+  \end{frame}
+
+  \begin{frame}
+    %% here the rules that differentiate System F from simply typed lambda calculus: abstraction and application.
+    %% again the modality is simply carried over.
+    \fboxsep=0pt
+    \noindent
+    \begin{minipage}[t]{0.40\linewidth}
+      \begin{center}
+        \bluetext{System F}
+      \end{center}
+      \small{
+        \inference[T-ABS]
+        {(\Gamma, \alpha) |- \graytext{t:}\ B} % chktex 1
+        {\Gamma |- \graytext{\Lambda \alpha.t:}\ \forall \alpha.B} % chktex 1
+        \vspace{2em}
+        \inference[T-APP]
+        {\Gamma |- \graytext{t:}\ \forall \alpha. B \quad \Gamma |- A} % chktex 1
+        {\Gamma |- \graytext{t \cdot A:}\ B[A/\alpha]} % chktex 1
+      }
+    \end{minipage}
+    \hfill
+    \begin{minipage}[t]{0.55\linewidth}
+      \begin{center}
+        \bluetext{\(\Lambda^p\)}
+      \end{center}
+      \small{
+        \inference[T-ABS]
+        {\rd{\gamma} (\Gamma, \alpha) |- \graytext{t:}\ B} % chktex 1
+        {\rd{\gamma}\Gamma |- \graytext{\Lambda \alpha.t:}\ \forall \alpha. B} % chktex 1
+        \vspace{2em}
+        \inference[T-APP]
+        {\rd{\gamma}\Gamma |- \graytext{t:}\ \forall \alpha. B \quad \Gamma |- A} % chktex 1
+        {\rd{\gamma}\Gamma |- \graytext{t\cdot A:}\ B[A/\alpha]} % chktex 1
+      }
+    \end{minipage}
+  \end{frame}
+
+  \begin{frame}
+    %% the introduction rule simply works by multiplying p
+    %% the elimination rule is more involved: first gamma produces p A, but to use A to produce C, we might need more than p, so we allow for an additional arbitrary multiplication by q
+    %% to give more flexibility to the grammar
+
+    \begin{center}
+      \bluetext{\(\Lambda^p\)}
+    \end{center}
+    \inference[p\(\langle\cdot\rangle\)-INTRO]
+    {\gamma \Gamma |- \graytext{t:} A} % chktex 1
+    {p\gamma\Gamma |- \graytext{[\leftindex^{p}t]:} p \langle A \rangle} % chktex 1
+
+    \vspace{2em}
+    \inference[p\(\langle\cdot\rangle\)-ELIM]
+    {\gamma\Gamma |- \graytext{u:} p\langle A \rangle \quad \delta \Gamma\graytext{, x:} \leftindex^{qp}A |- \graytext{t:} C} % chktex 1
+    {(q\gamma + \delta)\Gamma |-\graytext{\texttt{let} [\leftindex^{p}x] = \leftindex^{q} u \texttt{ in } t:} C} % chktex 1
+  \end{frame}
+
+  \begin{frame}
+    %% we note that every variable occurrence corresponds to usage 1. This ensures stability of usage under variable substitution. Other rules make modalities match.
+    %% for example abstraction introduces a variable with modality q and application multiplies the usage of the argument by q
+    \begin{center}
+      \hspace{-1em}\inference[WK]
+      {\delta \Gamma |- \graytext{t:} A \quad \gamma \leq \delta} % chktex 1
+      {\gamma\Gamma |- \graytext{t:} A} % chktex 1
+    \end{center}
+
+    \begin{theorem}[Convertibility]
+      If \(p \leq q\), then there is a term of type \(\leftindex^{p}A \to q \langle A \rangle \) for any \(A\).
+    \end{theorem}
+
+    %% it is allowed to use weakening: one can always use a variable in a more specific modality.
+    %% there is always convertibility in this direction
+
+    %% finally the existence of meet ensures compositionality for case branches.
+    %% that is if there are different branches, one can always find a single modality context such that it is smaller or equal than all the branches.
+  \end{frame}
+\end{section}
+
+\AtBeginSection[ ]
+{
+\begin{frame}{Outline}
+    \tableofcontents[currentsection]
+\end{frame}
+}
+
+\begin{section}{Applications}
+  \begin{frame}
+    %% While the origin of the discovery of this new logic comes from a semantical analysis of the models of System F (or polymorphic λ-calculus),
+    %% one can see the whole system of linear logic as a bold attempt to reconcile the beauty and symmetry of classical logic afforded by De Morgan's dualities
+    %% with the quest for constructive proofs that had led to intuitionistic logic.
+
+    Consider the three basic structural properties satisfied by simply-typed lambda calculus:
+
+    \begin{definition}[Exchange]
+      Exchange indicates that the order in which we write down variables in the context is irrelevant:
+
+      \begin{center}
+        \begin{tikzpicture}[node/.style = {draw,rounded corners,blur shadow, fill=white,align=center}]
+          \node[node] at (0.2,0) (if) {If\quad \(\Gamma_1, x_1 : T_1, x_2: T_2, \Gamma_2 \vdash t : T\)};
+          \node[node] at (0,-1.5) (then) {then\quad \(\Gamma_1, x_2 : T_2, x_1: T_1, \Gamma_2 \vdash t : T\)};
+
+          \draw[-{Stealth[length=2mm]}] (-0.78,-0.3) -- (0.54,-1.2);
+          \draw[-{Stealth[length=2mm]}] (0.54,-0.3) -- (-0.78,-1.2);
+        \end{tikzpicture}
+      \end{center}
+    \end{definition}
+
+  \end{frame}
+
+  \begin{frame}
+    \begin{definition}[Weakening]
+      Weakening indicates that adding extra unneeded assumptions to the context does not prevent a term from type checking:
+
+      \begin{center}
+        \begin{tikzpicture}[node/.style = {draw,rounded corners,blur shadow, fill=white,align=center}]
+          \node[node] at (-0.1,0) (if) {If\hspace{2.5em} \(\Gamma_1, \Gamma_2 \vdash t : T\)};
+          \node[node] at (0,-0.85) (then) {then\hspace{1em} \(\Gamma_1, x_1 : T_1, \Gamma_2 \vdash t : T\)};
+        \end{tikzpicture}
+      \end{center}
+    \end{definition}
+  \end{frame}
+
+  \begin{frame}
+    \begin{definition}[Contraction]
+      Contraction states that if we can type check a term using two identical assumptions (\(x_2:T_1\) and \(x_3:T_1\)) then we can check the same term using a single assumption:
+
+      \begin{center}
+        \begin{tikzpicture}[node/.style = {draw,rounded corners,blur shadow, fill=white,align=center}]
+          \node[node] at (-0.1,0) (if) {If\hspace{2.5em} \(\Gamma_1, x_2 : T_1, x_3 : T_1,\Gamma_2 \vdash t : T_2\)};
+          \node[node] at (0,-0.85) (then) {then\hspace{1em} \(\Gamma_1, x_1:T_1, \Gamma_2 \vdash [x_2 \mapsto x_1][x_3 \mapsto x_1] t : T_2\)};
+        \end{tikzpicture}
+      \end{center}
+    \end{definition}
+  \end{frame}
+
+  \begin{frame}
+    We thus have different types systems if we allow different rules to be applied:
+
+    \begin{itemize}
+    \item \bluetext{{\it Linear\/} type systems ensure that every variable is used exactly once (E)}.
+
+    \item {\it Affine\/} type systems ensure that every variable is used at most once (E, W).
+
+    \item {\it Relevant\/} type systems ensure that every variable is used at least once (E, C).
+
+    \item {\it Ordered\/} type systems ensure that every variable is used exactly once and in the order which it is introduced (none).
+    \end{itemize}
+  \end{frame}
+
+  \begin{frame}
+    %% omega, or also called \mathbb{N}, is the extremum of the meet-lattice.
+    %% variables associated with this modality can be used in unrestricted fashion.
+    \begin{center}
+      \begin{tikzpicture}[
+        node/.style = {draw,rounded corners,blur shadow,fill=white,align=center},
+        nodeh/.style = {},
+        nodegroup/.style = {draw,rounded corners,align=center}
+        ]
+        \onslide<1->{
+          \node[node] at (0,1.5) (linear) {linear (E)};
+          \node[node] at (-2,3) (affine) {affine (E, W)};
+          \node[node] at (2,3) (relevant) {relevant (E, C)};
+        }
+        \onslide<1>{
+          \node[node] at (0,0) (ordered) {ordered (none)};
+          \node[node] at (0,4.5) (unrestricted) {unrestricted (E, W, C)};
+        }
+
+        \onslide<1>{
+          \draw[-] (ordered) -- (linear);
+          \draw[-] (relevant) -- (unrestricted);
+          \draw[-] (affine) -- (unrestricted);
+        }
+
+        \onslide<1->{
+          \draw[-] (linear) -- (affine);
+          \draw[-] (linear) -- (relevant);
+        }
+
+        \onslide<2->{
+          \begin{scope}[node distance=0.3cm]
+            \node[nodeh] at (0,-0.2) (linearw) {\(\omega\)};
+            \node[nodeh] (linear0) [above left=of linearw] {0};
+            \node[nodeh] (linear1) [above right=of linearw] {1};
+            \draw[-] (linearw) -- (linear0);
+            \draw[-] (linearw) -- (linear1);
+          \end{scope}
+          \node[nodegroup,fit=(linearw)(linear0)(linear1)] (grouplinear) {};
+          \draw[-] (linear) -- (grouplinear);
+
+          \begin{scope}[node distance=0.3cm]
+            \node[nodeh] at (4,4) (linearw) {\(\omega\)};
+            \node[nodeh] (linear0) [above left=of linearw] {0};
+            \node[nodeh] (linear1p) [above right=of linearw] {\(1^{+}\)};
+            \draw[-] (linearw) -- (linear0);
+            \draw[-] (linearw) -- (linear1p);
+          \end{scope}
+          \node[nodegroup,fit=(linearw)(linear0)(linear1p)] (grouprelevant) {};
+          \draw[-] (relevant) -- (grouprelevant);
+
+          \begin{scope}[node distance=0.3cm]
+            \node[nodeh] at (-4,4) (linearw) {\(\omega\)};
+            \node[nodeh] (linearat) [above=of linearw] {@};
+            \node[nodeh] (linear0) [above=of linearat] {0};
+            \node[nodeh] (linear1) [right=of linearat] {\hspace{-0.9em}\(= 1\)};
+
+            \draw[-] (linearw) -- (linearat);
+            \draw[-] (linearat) -- (linear0);
+          \end{scope}
+          \node[nodegroup,fit=(linearw)(linearat)(linear0)(linear1)] (groupaffine) {};
+          \draw[-] (affine) -- (groupaffine);
+        }
+
+        \onslide<3->{
+          \begin{scope}[node distance=0.3cm]
+            \node[nodeh] at (-3,0) (linearw) {\(\omega\)};
+            \node[nodeh] (linearat) [above=of linearw] {@};
+            \node[nodeh] (linear1p) [right=of linearat] {\(1^{+}\)};
+            \node[nodeh] (linear1) [above=of linear1p] {1};
+            \node[nodeh] (linear0) [above left=of linearat] {0};
+            \draw[-] (linearw) -- (linear1p);
+            \draw[-] (linearw) -- (linearat);
+            \draw[-] (linearat) -- (linear0);
+            \draw[-] (linearat) -- (linear1);
+            \draw[-] (linear1p) -- (linear1);
+          \end{scope}
+          \node[
+          label={[label distance=0cm]-90:{\it combined}},
+          nodegroup,fit=(linearw)(linearat)(linear1p)(linear1)(linear0)] (groupcombined) {};
+        }
+      \end{tikzpicture}
+    \end{center}
+
+    %% It might be possible to define type systems containing other combinations
+    %% of structural properties, such as contraction only or weakening only,
+    %% but so far researchers have not found applications for such combinations.
+    %% Consequently, we have excluded them from the diagram.
+  \end{frame}
+
+  \begin{frame}\frametitle{Linear Types}
+    \vspace{1.5em}
+
+    Indeed the unit modality precisely corresponds to linear usages.
+
+    A 0-qualified function is necessarily constant ({\it irrelevance\/}).
+
+    \(\omega\) represents non-linear usage, equivalent to the more traditional exclamation mark (!).
+
+    \begin{tikzpicture}[
+      remember picture,overlay,
+      node/.style = {draw,rounded corners,blur shadow,fill=white,align=center},
+      nodeh/.style = {},
+      nodegroup/.style = {draw,rounded corners,align=center}
+      ]
+      \begin{scope}[node distance=0.3cm]
+        \node[nodeh,xshift=-3cm,yshift=-3.5cm] at (current page.north east) (linearw) {\(\omega\)};
+        \node[nodeh] (linear0) [above left=of linearw] {0};
+        \node[nodeh] (linear1) [above right=of linearw] {1};
+        \draw[-] (linearw) -- (linear0);
+        \draw[-] (linearw) -- (linear1);
+      \end{scope}
+      \node[nodegroup,fit=(linearw)(linear0)(linear1)] (grouplinear) {};
+    \end{tikzpicture}
+  \end{frame}
+
+
+  \begin{frame}\frametitle{Linear Type System}
+    \begin{center}
+      \begin{grammar}
+        \firstcase{A}{p \gralt{} p^{\bot}}{}
+        \otherform{A \otimes{} A \gralt{} A \oplus{} A}{}
+        \otherform{A \& A \gralt{} A \parr{} A}{}
+        \otherform{1 \gralt{} 0 \gralt{} \top{} \gralt{} \bot{}}{}
+        \otherform{!A \gralt{}?A}{}
+      \end{grammar}
+    \end{center}
+    %% where p are logical atoms
+
+    %% in particular we are intereseted in the exponentials: ! and ?, which limit access to weakening and contraction.
+    %% while in intuitionistic and constructive logic, the formula A \impl B can be interpreted as "if you give me an A, i will give you a B", in linear logic it means "give me as many A's as I might need and I will give you one B".
+    %% Encoding the notion of copy into the logic.
+
+    %% This duplication of the connectives actually leads to a much clearer understanding of the conflict between classical and intuitionistic logic.
+    %% For example, the law of excluded middle (A or not-A) is considered valid in the classical world and absurd in the intuitionistic one.
+    %% But in linear logic, this law has two readings: the additive version (A \oplus ¬A) is not provable and corresponds to the intuitionistic reading of disjunction;
+    %% the multiplicative version (A \parr \neg A) is trivially provable and simply corresponds to the tautology (A \implies A)
+    %% that is perfectly acceptable in intuitionistic logic too.
+  \end{frame}
+
+  \begin{frame}
+    %% the exponential ! (of course) permits contraction and weakening on the left sequent context, while the exponential ? (why not) permits contraction and weakening on the right hand sequent context.
+    The intuitionistic implication \(B \implies C \) can be defined as \( ! B \multimap C \)
+
+    Where \[ B \multimap A \triangleq B^\bot \parr C \]
+  \end{frame}
+
+  \begin{frame}
+    %% we must not forget the other two operations: addition and multiplication, but they follow an easily computable rules:
+
+    Finally the rules for \(\cdot\) and +:
+
+    \begin{center}
+      \begin{tblr}{c|ccccc}
+        (+) & 0 & \(\omega\) & @ & 1 & \(1^{+}\)\\
+        \midrule
+        0 & 0 & \(\omega\) & @ & 1 & \(1^{+}\) \\
+        \(\omega\) & \(\omega\) & \(\omega\) & \(\omega\) & \(1^{+}\) & \(1^{+}\) \\
+        @ & @ & \(\omega\) & \(\omega\) & \(1^{+}\) & \(1^{+}\) \\
+        1 & 1 & \(1^{+}\) & \(1^{+}\) & \(1^{+}\) & \(1^{+}\) \\
+        \(1^{+}\) & \(1^{+}\) & \(1^{+}\) & \(1^{+}\) & \(1^{+}\) & \(1^{+}\) \\
+      \end{tblr}\hspace{0.1em}
+      \begin{tblr}{c|ccccc}
+        \((\cdot)\) & 0 & \(\omega\) & @ & 1 & \(1^{+}\)\\
+        \midrule
+        0 & 0 & 0 & 0 & 0 & 0 \\
+        \(\omega\) & 0 & \(\omega\) & \(\omega\) & \(\omega\) & \(\omega\) \\
+        @ & 0 & \(\omega\) & @ & @ & \(\omega\) \\
+        1 & 0 & \(\omega\) & @ & 1 & \(1^{+}\) \\
+        \(1^{+}\) & 0 & \(\omega\) & \(\omega\) & \(1^{+}\) & \(1^{+}\) \\
+      \end{tblr}
+    \end{center}
+  \end{frame}
+
+  \begin{frame}\frametitle{Quantitative Typing}
+    A generalisation of all the above systems in what can be called quantitative typing, with one modality for each set of accepted usage.
+
+    %% modalities are interpreted as a sets of natural numbers.
+    %% An element in such a set is an admissible number of times that a variable can be used.
+
+    Where the set of all modalities Mod \(= 2^{\mathbb{N}}\), with \(0 = \{0\}, 1 = \{1\}\) and:
+    \begin{align*}
+      p+q &= \{x+y | x \in p, y \in q\}\\
+      p\cdot q &= \{x \cdot y | x \in p, y \in q\}\\
+      p \land q &= p \cup q
+    \end{align*} %% Minkovski operations
+
+    Every acceptable set of usage is tracked.
+    %% unfortunately even in their simplest form modality expressions for this structure can be too large.
+  \end{frame}
+
+  \begin{frame}\frametitle{Sensitivity Analysis for Differential Privacy}
+    In differential privacy one is interested in publishing statistically anonymised data without revealing individual secrets.
+
+    The role of the type system is to ensure that if a certain amount of noise is introduced in the inputs of a program, then at least the same amount is present in the outputs.
+  \end{frame}
+
+  \begin{frame}
+    In the literature every type \(A\) is equipped with a metric \(d_A : A \times A \to \mathbb{R}^{\infty}_{\geq 0}\).
+
+    \(f:A \to B\) is \(c\)-sensitive if it does not increase distances by a factor greater than \(c\):
+
+    \[d_B (f(x),f(y)) \leq_{\mathbb{R}} c \cdot d_A (x, y) \]
+    %% 0 means equality on all types \implies 0-sensitive functions are necessarily constant.
+    %% \infty-sensitive functions impose no restrictions on the argument.
+  \end{frame}
+
+  \begin{frame}
+    To translate the model into the proposed framework, let the modality carrier set be \(\mathbb{R}_{\geq 0}^{\infty}\); let \(\land\) be the max operator.\vspace{2em}
+
+    \bluetext{Note:} the order on the lattice is opposite to the order on \(\mathbb{R}\): \((\leq) = (\geq_{\mathbb{R}})\).
+  \end{frame}
+
+  \begin{frame}
+    In the literature there is a need to prove that evaluation preserve sensitivity, in this framework no special preservation proof is needed: any system is type-preserving for any modality ringoid, thus any assignment of types to metrics will do.
+  \end{frame}
+
+  \begin{frame}\frametitle{Information-Flow Security}
+    %% finally an application where it does not matter how many times variables are used, but rather in which context.
+    One application of type systems is to ensure that certain parts of a program do not have access to private (high security) information.\vspace{1em}
+
+    The principal property of such systems is that the output of a program does not depend on secret inputs.\vspace{1em}
+
+    This property holds for \(\Lambda^p\), if we consider that any modality \(p\) above 1 in the lattice is secret.
+    %% The simplest security lattice has a single secret level H (high) which can be represented by 0 and a single public level L (low) represented by 1
+  \end{frame}
+
+  \begin{frame}
+    \bluetext{Note:} The addition is relegated to play the same role as the meet: \((+) = (\land)\).
+
+    If we need a variable in two parts of a term, we mus assume the worst and require the most public level given by the meet.\vspace{1em}
+
+    \bluetext{Note:} The multiplication acts as the join (\(\lor\)) of the lattice (dual to the meet).
+
+    \begin{center}
+      \phantom{}
+      \inference[]
+      {|- t: \leftindex^{p}A -> B & x:  \leftindex^{q}X |- u: A}
+      {x: \leftindex^{p\lor{} q} X |- t \leftindex^{p} u: B}
+    \end{center}
+
+    %% Supporting security features via generic abstraction features of type systems have been proposed
+    %% before, but so far this has been done via quantification over types
+  \end{frame}
+\end{section}
+
+%%% Local Variables:
+%%% TeX-command-extra-options: "-shell-escape"
+%%% TeX-master: "document.tex"
+%%% End:

test/dune

@@ -25,3 +25,7 @@
 (test
  (name testingTypeFunParser)
  (libraries miniFun))
+
+(test
+ (name testingPolyFunParser)
+ (libraries miniFun))

test/testingPolyFunParser.expected

@@ -0,0 +1,11 @@
+Error absent assignment program: error (success)
+Error wrong input type program: error (success)
+Error not a function program: error (success)
+Error if branches with different types program: error (success)
+Error if guard is not a boolean program: error (success)
+Identity program: success
+Constant program: success
+Partial application of function program: success
+Passing functions to functions program: success
+Scope program: success
+Rand program: success

test/testingPolyFunParser.ml

@@ -0,0 +1,138 @@
+open MiniFun
+
+let get_result x =
+  Lexing.from_string x
+  |> Parser.prg Lexer.lex
+  |> TypeChecker.typecheck_polymorphic
+
+(* -------------------------------------------------------------------------- *)
+(* Error absent assignment program *)
+
+let program =
+  "lambda a: int -> int => x"
+;;
+
+Printf.printf "Error absent assignment program: ";
+match get_result program with
+  Error (`AbsentAssignment _) -> Printf.printf "error (success)\n"
+| _ -> Printf.printf "failed\n"
+
+(* -------------------------------------------------------------------------- *)
+(* Error wrong input type program *)
+
+let program =
+  "(lambda a: int -> int => a) false"
+;;
+
+Printf.printf "Error wrong input type program: ";
+match get_result program with
+  Error (`WrongType _) -> Printf.printf "error (success)\n"
+| _ -> Printf.printf " failed\n"
+
+(* -------------------------------------------------------------------------- *)
+(* Error not a function program *)
+
+let program =
+  "0 false"
+;;
+
+Printf.printf "Error not a function program: ";
+match get_result program with
+  Error (`WrongType _) -> Printf.printf "error (success)\n"
+| _ -> Printf.printf " failed\n"
+
+(* -------------------------------------------------------------------------- *)
+(* Error if branches with different types program *)
+
+let program =
+  "lambda x: int -> int => if 1 == 2 then true else 1"
+;;
+
+Printf.printf "Error if branches with different types program: ";
+match get_result program with
+  Error (`WrongType _) -> Printf.printf "error (success)\n"
+| _ -> Printf.printf " failed\n"
+
+(* -------------------------------------------------------------------------- *)
+(* Error if guard is not a boolean program *)
+
+let program =
+  "lambda x: int -> int => (if 1 then 2 else 1)"
+;;
+
+Printf.printf "Error if guard is not a boolean program: ";
+match get_result program with
+  Error (`WrongType _) -> Printf.printf "error (success)\n"
+| _ -> Printf.printf " failed\n"
+
+
+(* -------------------------------------------------------------------------- *)
+(* Identity program *)
+let program =
+  "lambda a: int -> int => a"
+;;
+
+Printf.printf "Identity program: ";
+match get_result program with
+  Ok _ -> Printf.printf "success\n"
+| _ -> Printf.printf " failed\n"
+
+(* -------------------------------------------------------------------------- *)
+(* Constant program *)
+let program =
+  "lambda a: int -> int => 1"
+;;
+
+Printf.printf "Constant program: ";
+match get_result program with
+  Ok _ -> Printf.printf "success\n"
+| _ -> Printf.printf " failed\n"
+
+(* -------------------------------------------------------------------------- *)
+(* Partial application of function program *)
+let program =
+  "let f = lambda x: int -> int -> int => lambda y: int -> int => x + y in f 3"
+;;
+
+Printf.printf "Partial application of function program: ";
+match get_result program with
+  Ok _ -> Printf.printf "success\n"
+| _ -> Printf.printf " failed\n"
+
+(* -------------------------------------------------------------------------- *)
+(* Passing functions to functions program *)
+let program =
+  "let f =
+     \\z: (int -> int) -> (int -> int) -> int -> int =>
+       \\y: (int -> int) -> int -> int =>
+         \\x: int -> int =>
+           if x < 0 then y x else z x
+   in (f (\\x: int -> int => x + 1)) (\\x: int -> int => x - 1)"
+;;
+
+Printf.printf "Passing functions to functions program: ";
+match get_result program with
+  Ok _ -> Printf.printf "success\n"
+| _ -> Printf.printf " failed\n"
+
+(* -------------------------------------------------------------------------- *)
+(* Scope program *)
+let program =
+  "let f = let a = 1 in fun y: int -> int => y + a in let a = 2 in f"
+;;
+
+Printf.printf "Scope program: ";
+match get_result program with
+  Ok _ -> Printf.printf "success\n"
+| _ -> Printf.printf " failed\n"
+
+(* -------------------------------------------------------------------------- *)
+(* Rand program *)
+let program =
+  "fun x: int -> int => rand x"
+;;
+
+Printf.printf "Rand program: ";
+match get_result program with
+  Ok _ -> Printf.printf "success\n"
+| _ -> Printf.printf " failed\n"