@ -6,12 +6,19 @@ type type_error =
| NotAnArrow of debruijn_type
| NotAProduct of debruijn_type
| NotAForall of debruijn_type
| NotAnEqual of debruijn_type
| UnboundTermVariable of tevar
| UnboundTypeVariable of tyvar
| TwoOccurencesOfSameVariable of string
| ContextNotAbsurd
| UnexpectedRecord
| DeclarationNotFound of Datatype . tyconstr_id
| LabelNotFound of Datatype . label_id
and arity_requirement = Index of int | Total of int
exception TypeError of type_error
exception TypeError of loc * type_error
(* -------------------------------------------------------------------------- *)
@ -37,58 +44,99 @@ module TermVarMap =
module N2DB =
DeBruijn . Nominal2deBruijn ( TermVar )
(* We use a union-find data structure to represent equalities between rigid
variables and types . We need the ability to snapshot and rollback changes , to
undo the addition of an equality to the environment . * )
module UF = struct
include UnionFind . Make ( UnionFind . StoreVector )
type ' a elem = ' a rref
end
module S =
Structure
(* We translate types into union-find graphs to check equality.
μ - types create cyclic graphs . Each vertex represents a type expression .
GADTs can add type equalities in the context and we represent
this by unifying their vertices in the union - find graph . This is
possible only when they have compatible structures ( or one of the
side has no structure ) , otherwise the equality is inconsistent . * )
type vertex =
structure option UF . elem
and structure =
(* Corresponds to types from the source language ( arrow, product, ... ) . *)
| SStruct of vertex S . structure
(* Represents ∀α.τ. We use De Bruijn levels, so we don't need to name
explicitly the bound variable α . * )
| SForall of vertex
(* A De Bruijn level corresponding to a ∀-bound variable. Using levels
instead of indices makes the equality test easier . * )
| SForallLevel of int
(* The global store of the union-find. *)
type uf_store = structure option UF . store
(* A mapping from rigid variables to union-find vertices. *)
type uf_tyvars = structure option UF . elem list
(* If the type equations introduced are inconsistent, then no need for
[ store ] and [ tyvars ] * )
type equations_env =
| Equations of { store : uf_store ; tyvars : uf_tyvars }
| Inconsistent
type env = {
(* A mapping of term variables to types. *)
types : debruijn_type TermVarMap . t ;
(* A translation environment of TERM variables to TYPE indices. *)
names : N2DB . env ;
(* We keep trace of whether or not the typing equations is consistent *)
equations : equations_env ;
}
type _ datatype_env = ( unit , debruijn_type ) Datatype . Env . t
let empty =
{ types = TermVarMap . empty ; names = N2DB . empty }
let empty = {
types = TermVarMap . empty ;
names = N2DB . empty ;
equations = Equations { store = UF . new_store () ; tyvars = [] } ;
}
let lookup { types ; names } x =
try
(* Obtain the type associated with [x]. *)
let ty = TermVarMap . find x types in
let lookup ~ loc { types ; names ; _ } x =
(* Obtain the type associated with [x]. *)
match TermVarMap . find x types with
| exception Not_found ->
raise ( TypeError ( loc , UnboundTermVariable x ) )
| ty ->
(* Find how long ago [x] was bound. *)
let w = N2DB . lookup names x in
(* Shift the type [ty] by this amount, so that it makes sense in the
current scope . * )
Type . lift w 0 ty
with Not_found ->
(* must have been raised by [TermVarMap.find] *)
raise ( TypeError ( UnboundTermVariable x ) )
let extend_with_tevar { types ; names } x ty =
let extend_with_tevar { types ; names ; equations } x ty =
(* Map the name [x] to [ty], and record when it was bound, without
incrementing the time . * )
{ types = TermVarMap . add x ty types ;
names = N2DB . slide names x }
let extend_with_tyvar { types ; names } =
(* Increment the time. *)
{ types ; names = N2DB . bump names }
let singleton x ty =
extend_with_tevar empty x ty
let concat env1 env2 =
let combine _ _ ty2 = Some ty2 in
{ types = TermVarMap . union combine env1 . types env2 . types ;
names = N2DB . concat env1 . names env2 . names }
let concat_disjoint env1 env2 =
let exception Conflict of TermVarMap . key in
try
let combine x _ _ =
raise ( Conflict x ) in
let types = TermVarMap . union combine env1 . types env2 . types
and names = N2DB . concat env1 . names env2 . names in
Ok { types ; names ; }
with Conflict x -> Error x
names = N2DB . slide names x ;
equations ; }
let extend_with_tevar_no_dup ~ loc ( { types ; _ } as env ) x ty =
if TermVarMap . mem x types then
raise ( TypeError ( loc , TwoOccurencesOfSameVariable x ) ) ;
extend_with_tevar env x ty
let extend_with_tyvar { types ; names ; equations } =
match equations with
| Inconsistent ->
{ types ; names ; equations }
| Equations { store ; tyvars } ->
(* Create a fresh vertex for the new type variable *)
let v = UF . make store None in
(* Extend the environment of type variables *)
let tyvars = v :: tyvars in
(* Increment the time. *)
let names = N2DB . bump names in
{ types ; names ; equations = Equations { store ; tyvars } }
(* -------------------------------------------------------------------------- *)
@ -101,95 +149,32 @@ let unfold ty =
| _ ->
assert false
let rec as_arrow ty =
let rec as_arrow ~ loc ty =
match ty with
| TyArrow ( ty1 , ty2 ) ->
ty1 , ty2
| TyMu _ ->
as_arrow unfold ty )
as_arrow ~loc (unfold ty )
| _ ->
raise ( TypeError ( NotAnArrow ty ) )
raise ( TypeError ( loc , NotAnArrow ty ) )
let rec as_product ty =
let rec as_product ~ loc ty =
match ty with
| TyProduct tys ->
tys
| TyMu _ ->
as_product unfold ty )
as_product ~loc (unfold ty )
| _ ->
raise ( TypeError ( NotAProduct ty ) )
raise ( TypeError ( loc , NotAProduct ty ) )
let rec as_forall ty =
let rec as_forall ~ loc ty =
match ty with
| TyForall ( () , ty ) ->
ty
| TyMu _ ->
as_forall unfold ty )
as_forall ~loc (unfold ty )
| _ ->
raise ( TypeError ( NotAForall ty ) )
(* -------------------------------------------------------------------------- *)
(* [equal1] groups the easy cases of the type equality test. It does not
accept arguments of the form [ TyMu ] . It expects a self parameter [ equal ]
that is used to compare the children of the two root nodes . * )
let pointwise equal tys1 tys2 =
try
List . for_all2 equal tys1 tys2
with Invalid_argument _ ->
(* Catching [Invalid_argument] is bad style, but saves a couple calls
to [ List . length ] . A cleaner approach would be to use arrays instead
of lists . * )
false
let equal1 equal ty1 ty2 =
match ty1 , ty2 with
| TyMu _ , _
| _ , TyMu _ ->
assert false
| TyVar x1 , TyVar x2 ->
Int . equal x1 x2
| TyArrow ( ty1a , ty1b ) , TyArrow ( ty2a , ty2b ) ->
equal ty1a ty2a && equal ty1b ty2b
| TyForall ( () , ty1 ) , TyForall ( () , ty2 ) ->
equal ty1 ty2
| TyProduct tys1 , TyProduct tys2 ->
pointwise equal tys1 tys2
| TyConstr ( Datatype . Type tyconstr1 , tys1 ) ,
TyConstr ( Datatype . Type tyconstr2 , tys2 ) ->
String . equal tyconstr1 tyconstr2 &&
pointwise equal tys1 tys2
| ( TyVar _ | TyArrow _ | TyForall _ | TyProduct _ | TyConstr _ ) ,
_ ->
false
(* -------------------------------------------------------------------------- *)
(* An unsound approximation of the equality test. ( Now unused. ) *)
(* Comparing two [TyMu] types simply by comparing their bodies would be
correct , but incomplete : some types that are equal would be considered
different . * )
(* Naively unfolding every [TyMu] type is sound and complete, but leads to
potential non - termination . The following code avoids non - termination by
imposing a budget limit . This makes this equality test unsound : two types
may be considered equal when they are in fact different . * )
let rec equal budget ty1 ty2 =
match ty1 , ty2 with
| ( TyMu _ as ty1 ) , ty2
| ty2 , ( TyMu _ as ty1 ) ->
budget = 0 | | equal ( budget - 1 ) ( unfold ty1 ) ty2
| _ , _ ->
equal1 ( equal budget ) ty1 ty2
let budget =
4
let _ unsound_equal ty1 ty2 =
equal budget ty1 ty2
raise ( TypeError ( loc , NotAForall ty ) )
(* -------------------------------------------------------------------------- *)
@ -197,204 +182,282 @@ let _unsound_equal ty1 ty2 =
(* The System F types produced by an ML type inference algorithm cannot
contain [ TyForall ] under [ TyMu ] . In this restricted setting , deciding
type equality is relatively easy . We proceed in two layers , as follows :
- Initially , we perform a normal ( structural ) equality test , going
down under [ TyForall ] constructors if necessary . As soon as we
hit a [ TyMu ] constructor on either side , we switch to the lower
layer :
- In the lower layer , we know that we cannot hit a [ TyForall ]
constructor ( if we do , we report that the types differ ) . We
map each type ( separately ) to a graph of unification variables
( where every variable has rigid structure ) , then we check that
the two graphs can be unified . * )
type equality is relatively easy . We map each type to a graph of
unification variables ( where every variable has rigid structure ) ,
then we check that the two graphs can be unified . * )
exception Clash =
Structure . Iter2
module S =
Structure
type vertex =
structure UnionFind . elem
and structure =
| SRigidVar of DeBruijn . index
| SStruct of vertex S . structure
let rec translate ( env : vertex list ) ( ty : F . debruijn_type ) : vertex =
match ty with
(* This function assumes no universal quantification inside a μ-type, because
it would be difficult to check type equality otherwise . The boolean
[ inside_mu ] tracks whether we are already under a μ quantifier . * )
let rec translate ~ loc ~ inside_mu store ( env : vertex list ) ( ty : F . debruijn_type )
: vertex
= match ty with
| TyVar x ->
(* If [x] is bound in [env], then [x] is bound by μ, and we
already have a vertex that represents it . Otherwise , [ x ]
is bound by ∀ , and it is regarded as a rigid variable . * )
let n = List . length env in
if x < n then
List . nth env x
else
UnionFind . make ( SRigidVar ( x - n ) )
begin
(* If the type is closed, then [x] was bound by a quantifier before and
was added to the environment . * )
try
List . nth env x
with Not_found ->
raise ( TypeError ( loc , UnboundTypeVariable x ) )
end
| TyMu ( () , ty ) ->
(* Extend the environment with a mapping of this μ-bound variable
to a fresh vertex . * )
let dummy : structure = SRigidVar 0 in
let v1 = UnionFind . make dummy in
let v1 = UF . make store None in
let env = v1 :: env in
(* Translate the body. *)
let v2 = translate env ty in
let v2 = translate ~ loc ~ inside_mu : true store env ty in
(* Unify the vertices [v1] and [v2], keeping [v2]'s structure. *)
let v = U nion Find . merg e ( fun _ s2 -> s2 ) v1 v2 in
let v = U F. merg e stor e ( fun _ s2 -> s2 ) v1 v2 in
v
| TyForall _ ->
(* Either we have found a ∀ under a μ, which is unexpected, or one
of the types that we are comparing has more ∀ quantifiers than
the other . Either way , we report that the types differ . * )
raise Clash
| TyForall ( () , ty ) ->
assert ( not inside_mu ) ;
(* Extend the environment with a mapping of this forall-bound variable
to a fresh vertex . * )
let v1 = UF . make store ( Some ( SForallLevel ( List . length env ) ) ) in
let env = v1 :: env in
(* Translate the body. *)
let v2 = translate ~ loc ~ inside_mu store env ty in
UF . make store ( Some ( SForall v2 ) )
| TyArrow ( ty1 , ty2 ) ->
let v1 = translate env ty1
and v2 = translate env ty2 in
U nion Find . mak e ( SStruct ( S . TyArrow ( v1 , v2 ) ) )
let v1 = translate ~ loc ~ inside_mu store env ty1
and v2 = translate ~ loc ~ inside_mu store env ty2 in
U F. mak e store ( Som e ( SStruct ( S . TyArrow ( v1 , v2 ) ) ) )
| TyProduct tys ->
let vs = translate_list env tys in
U nion Find . mak e ( SStruct ( S . TyProduct vs ) )
let vs = translate_list ~ loc ~ inside_mu store env tys in
U F. mak e store ( Som e ( SStruct ( S . TyProduct vs ) ) )
| TyConstr ( id , tys ) ->
let vs = translate_list env tys in
UnionFind . make ( SStruct ( S . TyConstr ( id , vs ) ) )
let vs = translate_list ~ loc ~ inside_mu store env tys in
UF . make store ( Some ( SStruct ( S . TyConstr ( id , vs ) ) ) )
| TyEq ( ty1 , ty2 ) ->
let v1 = translate ~ loc ~ inside_mu store env ty1
and v2 = translate ~ loc ~ inside_mu store env ty2 in
UF . make store ( Some ( SStruct ( S . TyEq ( v1 , v2 ) ) ) )
and translate_list env tys =
List . map ( translate env ) tys
and translate_list ~ loc ~ inside_mu store env tys =
List . map ( translate ~ loc ~ inside_mu store env ) tys
let insert q v1 v2 =
Stack . push ( v1 , v2 ) q
let unify_struct q s1 s2 =
match s1 , s2 with
| S RigidVar x1 , SRigidVar x2 ->
| S ForallLevel x1 , SForallLevel x2 ->
if x1 < > x2 then raise Clash
| SStruct s1 , SStruct s2 ->
Structure . iter2 ( insert q ) s1 s2
| SRigidVar _ , SStruct _
| SStruct _ , SRigidVar _ ->
| SForall s1 , SForall s2 ->
insert q s1 s2
| SForallLevel _ , _
| SStruct _ , _
| SForall _ , _ ->
raise Clash
let merge_struct q s1 s2 =
unify_struct q s1 s2 ;
s1
let rec unify q ( v1 : vertex ) ( v2 : vertex ) =
let ( _ : vertex ) = UnionFind . merge ( merge_struct q ) v1 v2 in
unify_pending q
and unify_pending q =
(* We need two operations on equalities between types:
- add an equality to the equations in the environment
- check if a given equality holds modulo the equations in the environment * )
(* Both operations can be described as first decomposing a given equality
" ty1 = ty2 " into " simple equalities " between a rigid variable and a type .
In fact , the union - find data structure that we use to represent an
environment of equations store exactly those simple equalities . * )
(* Then:
- to add an equality , we modify our environment by unifying the type
variables with the equated type
- to check an equality , we check that the simple equalities are already
valid in the equations of the environment , and fail otherwise * )
(* The decomposition process does not produce simple equalities if the
provided equality is absurd ( " int * int = int * bool " ) .
Then :
- if we are adding this equality to the environment , we record that the
environment is now Inconsistent
- if we are checking the equality ( in a consistent environment ) , we fail * )
(* The functions below implement a unification procedure that implements both
these operations , depending on a [ mode ] parameter :
- in [ Input ] mode , they add an equality to the environment
- in [ Check ] mode , they check that the equality holds modulo the equations
in the environment * )
type mode = Input | Check
let merge_struct mode q so1 so2 : structure option =
match so1 , so2 with
| Some s1 , Some s2 ->
unify_struct q s1 s2 ;
so1
| None , so | so , None ->
match mode with
| Input ->
so
| Check ->
raise Clash
let rec unify mode store q ( v1 : vertex ) ( v2 : vertex ) =
let ( _ : vertex ) = UF . merge store ( merge_struct mode q ) v1 v2 in
unify_pending mode store q
and unify_pending mode store q =
match Stack . pop q with
| v1 , v2 ->
unify q v1 v2
unify mode store q v1 v2
| exception Stack . Empty ->
()
let unify v1 v2 =
let unify mode store v1 v2 =
let q = Stack . create () in
unify q v1 v2
let rec equal ty1 ty2 =
match ty1 , ty2 with
| ( TyMu _ as ty1 ) , ty2
| ty2 , ( TyMu _ as ty1 ) ->
(* We have hit a μ binder on one side. Switch to layer-1 mode. *)
begin try
let env = [] in
let v1 = translate env ty1
and v2 = translate env ty2 in
unify v1 v2 ;
true
with Clash ->
false
end
| _ , _ ->
(* Otherwise, continue in layer-2 mode. *)
equal1 equal ty1 ty2
unify mode store q v1 v2
let unify_types ~ loc mode env ty1 ty2 =
match env . equations with
| Inconsistent ->
true
| Equations { store ; tyvars } ->
try
let v1 = translate ~ loc ~ inside_mu : false store tyvars ty1
and v2 = translate ~ loc ~ inside_mu : false store tyvars ty2 in
unify mode store v1 v2 ;
true
with Clash ->
false
(* -------------------------------------------------------------------------- *)
(* Re-package the type equality test as a type equality check. *)
(* Re-package the type unification as a type equality check. *)
let enforce_equal ~ loc env ty1 ty2 : unit =
if not ( unify_types ~ loc Check env ty1 ty2 ) then
raise ( TypeError ( loc , TypeMismatch ( ty1 , ty2 ) ) )
let ( - - ) ty1 ty2 : unit =
if not ( equal ty1 ty2 ) then
raise ( TypeError ( TypeMismatch ( ty1 , ty2 ) ) )
(* Re-package the type unification as an addition in the environment. *)
let add_equation ~ loc env ty1 ty2 : env =
if unify_types ~ loc Input env ty1 ty2 then
env
else
{ env with equations = Inconsistent }
let copy_env env store tyvars =
let store_copy = UF . copy store in
let equations = Equations { store = store_copy ; tyvars } in
{ env with equations }
(* -------------------------------------------------------------------------- *)
(* The type-checker. *)
let nth_type ty tys i =
let nth_type ~ loc ty tys i =
if i < 0 | | i > = List . length tys then
raise ( TypeError ( ArityMismatch ( Index i , ty ) ) )
raise ( TypeError ( loc , ArityMismatch ( Index i , ty ) ) )
else
List . nth tys i
let rec typeof datatype_env env ( t : debruijn_term ) : debruijn_type =
let typeof = typeof datatype_env in
match t with
| Var ( _ , x ) ->
lookup env x
| Var ( loc , x ) ->
lookup ~ loc env x
| Hole ( _ , ty , ts ) ->
let on_subterm t =
ignore ( typeof env t ) in
List . iter on_subterm ts ;
ty
| Annot ( _ , t , ty ) ->
typeof env t - - ty ;
| Annot ( loc , t , ty ) ->
enforce_equal ~ loc env ( typeof env t ) ty ;
ty
| Abs ( _ , x , ty1 , t ) ->
let ty2 = typeof ( extend_with_tevar env x ty1 ) t in
TyArrow ( ty1 , ty2 )
| App ( _ , t , u ) ->
let ty1 , ty2 = as_arrow typeof env t ) in
typeof env u - - ty1 ;
| App ( loc , t , u ) ->
let ty1 , ty2 = as_arrow ~loc (typeof env t ) in
enforce_equal ~ loc env ( typeof env u ) ty1 ;
ty2
| Let ( _ , x , t , u ) ->
let env = extend_with_tevar env x ( typeof env t ) in
typeof env u
| Let ( loc , rec_ , x , ty , t , u ) ->
let env_with_x = extend_with_tevar env x ty in
let def_env = match rec_ with
| Non_recursive -> env
| Recursive -> env_with_x
in
enforce_equal ~ loc def_env ( typeof def_env t ) ty ;
typeof env_with_x u
| TyAbs ( _ , () , t ) ->
TyForall ( () , typeof ( extend_with_tyvar env ) t )
| TyApp ( _ , t , ty2 ) ->
Type . subst ty2 0 ( as_forall ( typeof env t ) )
| TyApp ( loc , t , ty2 ) ->
Type . subst ty2 0 ( as_forall ~loc (typeof env t ) )
| Tuple ( _ , ts ) ->
let tys = List . map ( typeof env ) ts in
TyProduct tys
| Proj ( _ , i , t ) ->
| Proj ( loc , i , t ) ->
let ty = typeof env t in
let tys = as_product ty in
nth_type ty tys i
| Variant ( _ , lbl , dty , t ) ->
let arg_type = typeof_variant datatype_env lbl dty in
let tys = as_product ~ loc ty in
nth_type ~ loc ty tys i
| Variant ( loc , lbl , dty , t ) ->
let arg_type = typeof_variant datatype_env ~ loc lbl dty in
let ty = typeof env t in
ty - - arg_type ;
enforce_equal ~ loc env ty arg_type
Gabriel Scherer
SCHERER Gabriel
Olivier
Alistair O'Brien