Skip to content

Latest commit

 

History

History
117 lines (96 loc) · 4.05 KB

TODO.md

File metadata and controls

117 lines (96 loc) · 4.05 KB
Raw

Basic types and functions:

  • Integer.
  • Boolean.
  • test (if .. then .. else ..)

Grammar.

  • Add let x : T = t to define top-level definition. It is used to extend the environment.

    • Add a magic term of type Nothing to define a term which has no implementation (like () for unit). With this term, we can say a term exist without defining the meaning.

  • Add (term : Type) with the typing rule: Γ ⊦ t : T => Γ ⊦ (t : T) : T

  • Add let x = t.

  • Reorganize the grammar because it's very ugly! let x : T = t is equivalent to let x = (t : T).

Subtyping.

  • Check all results.
  • Automatic verification for tests.
  • Add an history to get the derivation tree.
  • Use SUB in select rules.
  • Add an action to check if each algorithm outputs the same result. representation of a variable when an error occurs and is raised.
  • Trick when SEL <: and <: SEL can be both used.
  • Add let x = t.
  • check well formedness.

Not important.

  • Return all possible derivation trees.
  • Take an extend environment (Atom -> String) to recover the initial

Typing.

  • In let x = s in t, check that the variable doesn't appear in the type of t. This is the avoidance problem.
  • Add let x = t.
  • least_upper_bound_of_dependent_function: call to best_bounds and check if it's an arrow. If it's Nothing, we need to return Top -> Nothing because it's the least upper bound which is an arrow.
  • check best_bounds.
  • check well formedness.

Not important.

  • Improve error message in var application when we have x.A (for the moment, we only have x.A, not what is x.A). Example
  • Take an extend environment (Atom -> String) to recover the initial

Evaluation.

Not important.

  • Add a syntax to check typing at runtime like
[@check_typing type]

MISC

  • Add a function well_formed : env -> Grammar.nominal_typ -> bool returning true if the given nominal type is well formed. We say a type T is not well formed if T is the form x.A and x is not a variable of type { A : Nothing .. Any }.
  • Be able to extend the environment with the syntax let x : T = t.
  • Use a default environment (like Pervasives in OCaml) while reading a file.

Not important.

  • Emacs mode.

Surface language.

  • Add a sugar for dependent function when the variable is not needed in the return type.
  • type S : Nothing .. Any (no need to mention bounds) -> S
  • S : Nothing .. U -> S <: U
  • S : L .. Any -> S :> L
  • struct .. end (ou obj .. end) to define terms and sig .. end to define types.
  • sig S = int end for { S : int .. int } (so S = int is for terms and also for types, the difference is sig .. end and struct .. end)
  • Allow to use
sig
  type S = int.A
  type T = S
end

instead of

sig
  type S = int.A
  type T = self.S
end

It implies to remember the variable binding in the module.

  • Instead of z => sig .. end, use module z = struct .. end.
  • Instead of z => sig .. end, use module type z = sig .. end
  • Top level module definitions.
  • Top level module type definitions.
  • Top level type definitions. type T = int = let x = struct type T = int end in open x.
  • keyword include in modules.
  • keyword with type S = ... --> intersection.
  • Multiple argument.
  • Remove ;; for top level definitions. It implies to consider a file like a module.
  • Sugar for polymorphic types like type 'a t = 'a.
  • Recursive functions. How can we implement this?
  • Allow to write File.expression. It searches for the module File in the base_modules. base_modules a list of modules loaded with the command line. It can be files. If File is a file, then we can add a directory to search it with the argument -I.
  • open M = for all labels l in M, add M.l in the environment with the name l
  • t => struct .. end --> struct(t) .. end
  • function with multiple arguments.
  • infix operators.