Positive Subtyping in presence of Bounded Quantifiers
Standard ML
Switch branches/tags
Nothing to show
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
BQEnv.sig
BQEnv.sml
Bq.sml
CParserTest.sml
Compile.sml
Constraints.sig
Constraints.sml
DcTest.sml
Distances.sig
Distances.sml
DistancesTest.sml
EParserTest.sml
EnvTest.sml
Expressions.sml
FtvTest.sml
Inference.sig
Inference.sml
InferenceTest.sml
Main.sml
Makefile
Names.sml
NamesTest.sml
Parser.sig
Parser.sml
README.md
Set.sml
SmlUnit.sml
StringMap.sml
TParserTest.sml
Tokenizer.sig
Tokenizer.sml
TokenizerTest.sml
Types.sml
TypesTest.sml
WeakSatTest.sml
bq.cm
type-inference-positive-subtyping.pdf

README.md

Type Inference in Presence of Positive Subtyping

Prototype implementation of the type inference system described in this paper. You'll need SML/NJ to try it out.

For instance, typing the identify function fn x => x

$ sml -m bq.cm
...
- Bq.i "fn x => x";
fn x => x : \X1|true.X1 -> X1
val it = () : unit

Which correctly produces the polymorphic type X -> X. See the paper for additional examples you can try.