A library for constraint-based Hindley-Milner type inference
Library inferno
Module Inferno . Decoder . Make


module S : sig ... end
module U : sig ... end
module O : sig ... end


val decode_variable : U.variable -> O.tyvar

decode_variable v decodes the variable v.

val new_acyclic_decoder : unit -> U.variable -> O.ty

new_acyclic_decoder() initiates a new decoding phase. It returns a decoding function decode, which can be used as many as times as one wishes. Decoding requires the graph to be acyclic: it is a bottom-up computation. decode internally performs memoization, so even if the decoder is called many times, the total cost of decoding is linear in the size of the graph fragment that is decoded.

As a caveat that one must bear in mind, when the type ty of decoded types is a type of abstract syntax trees, then the decoder actually produces a DAG of type ty. Traversing this DAG in a naive way, without paying attention to the fact that some subtrees may be shared, can result in a traversal whose complexity is exponential.

val new_cyclic_decoder : unit -> U.variable -> O.ty

new_cyclic_decoder is analogous to new_acyclic_decoder, but tolerates cyclic graphs. The decoder detects cycles and uses the function mu to decode them into equirecursive types. The decoder performs memoization only at the vertices that do not participate in a cycle. This makes the complexity of decoding higher than the acyclic case, but we expect it to remain linear in practice.