UCSD-PL / refscript

Refinement Types for Scripting Languages
BSD 3-Clause "New" or "Revised" License
65 stars 3 forks source link

Polymorphic types and subtyping #46

Open panagosg7 opened 10 years ago

panagosg7 commented 10 years ago

Assume we have a type:

interface A {
  c: int;
  f: forall T . (T) => T; 
}

Then for doing the subtyping:

A <: { f: (int) => int }

we'd have to first unfold A into

{
  c: number;
  f: forall T . (T) => T; 
}

Then deeply instantiate all quantified types:

{
  c: number;
  f: (T0) => T0; 
}

Unify: T0 := int

Finally, do the subtyping:

{ c: number; f: (T0) => T0; } [T0: int] <: { f: (int) => int; } ~> UPCAST

Example: https://github.com/UCSD-PL/RefScript/blob/poly-subt/tests/pos/simple/contextual.ts