package catala

  1. Overview
  2. Docs
package catala
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Dcalc.TypingSource

Typing for the default calculus. Because of the error terms, we perform type inference using the classical W algorithm with union-find unification.

Sourcemodule Pos = Utils.Pos
Sourcemodule Errors = Utils.Errors
Sourcemodule A = Ast
Sourcemodule Cli = Utils.Cli

Types and unification

Sourcetype typ =
  1. | TLit of A.typ_lit
  2. | TArrow of typ Pos.marked UnionFind.elem * typ Pos.marked UnionFind.elem
  3. | TTuple of typ Pos.marked UnionFind.elem list
  4. | TEnum of typ Pos.marked UnionFind.elem list
  5. | 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.

Raises an error if unification cannot be performed

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

Double-directed typing

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

Infers the most permissive type from an expression

Sourceval 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 check_type : A.expr Pos.marked -> A.typ Pos.marked -> unit

Typechecks an expression given an expected type

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct