Typing (p.catala.0.2.0.doc.catala.dcalc.Dcalc.Typing)

Sourcemodule Pos = Utils.Pos

Sourcemodule Errors = Utils.Errors

Sourcemodule A = Ast

Sourcemodule Cli = Utils.Cli

Types and unification

Sourcetype typ =

| TLit of A.typ_lit
| TArrow of typ Pos.marked UnionFind.elem * typ Pos.marked UnionFind.elem
| TTuple of typ Pos.marked UnionFind.elem list
| TEnum of typ Pos.marked UnionFind.elem list
| TAny

We do not reuse Dcalc.Ast.typ because we have to include a new TAny variant. Indeed, error terms can have any type and this has to be captured by the type sytem.

Sourceval format_typ : Format.formatter -> typ Pos.marked UnionFind.elem -> unit

Source

val unify : 
  typ Pos.marked UnionFind.elem ->
  typ Pos.marked UnionFind.elem ->
  unit

Raises an error if unification cannot be performed

Sourceval op_type : A.operator Pos.marked -> typ Pos.marked UnionFind.elem

Operators have a single type, instead of being polymorphic with constraints. This allows us to have a simpler type system, while we argue the syntactic burden of operator annotations helps the programmer visualize the type flow in the code.

Sourceval ast_to_typ : A.typ -> typ

Sourceval typ_to_ast : typ Pos.marked UnionFind.elem -> A.typ Pos.marked

Double-directed typing

Sourcetype env = typ Pos.marked A.VarMap.t

Source

val typecheck_expr_bottom_up : 
  env ->
  A.expr Pos.marked ->
  typ Pos.marked UnionFind.elem

Infers the most permissive type from an expression

Source

val typecheck_expr_top_down : 
  env ->
  A.expr Pos.marked ->
  typ Pos.marked UnionFind.elem ->
  unit

Checks whether the expression can be typed with the provided type

API

Sourceval infer_type : A.expr Pos.marked -> A.typ Pos.marked

Sourceval check_type : A.expr Pos.marked -> A.typ Pos.marked -> unit

Typechecks an expression given an expected type