package catala
Install
Dune Dependency
Authors
Maintainers
Sources
md5=4c6f725ef4d21c5ff91f60d74b454ef7
sha512=98806e03daa6f33740b80a0f78a37320fb70ebea8cb927ea8fed022673459189c32e2389ccba0fa25d93f754b0fa0128a5ee28e1bb9abefa330deb4be8cc7d95
doc/catala.dcalc/Dcalc/Typing/index.html
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.
Types and unification
type 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.
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.
Double-directed typing
Infers the most permissive type from an expression
val typecheck_expr_top_down :
env ->
A.expr Pos.marked ->
typ Pos.marked UnionFind.elem ->
unitChecks whether the expression can be typed with the provided type
API
Typechecks an expression given an expected type