search

kongware / ftor

ftor enables ML-like type-directed, functional programming with Javascript including reasonable debugging.
MIT License
44 stars 1 forks source link

Missing Subsumption Rule #12

Closed ivenmarquardt closed 6 years ago

ivenmarquardt commented 6 years ago

The following application should be well-typed,

f :: a -> b -> b
g :: (a -> a -> a) -> Int

f g -- well-typed

because k is independently and thus more polymorphic than f expects for its function argument. A subsumption rule must also consider co-/contra-variance:

f :: ([b] -> [b] -> Int) -> Int
g :: a -> a -> Int

f g -- ill-typed
ivenmarquardt commented 6 years ago

Since I restrict polytypes to multi-constructor ADTs (sum type), there is currently no need to extend the type system with an additional subsumption rule. As soon as the type validator works stable and I've gained more experiences with HM, I probably retry to implement rank-n types. Then a subsumption rule becomes crucial again.