Infernu’s type system informal summary – first draft

I just finished a first draft describing Infernu’s type system. Target audience is potential users.

Comments welcome!

Infernu’s type system informal summary – first draft

3 thoughts on “Infernu’s type system informal summary – first draft

  1. An alternative to the value restriction, if you’re willing to stomach pervasive higher rank types, is to have variables introduce a rigid binding, in the MLF sense. This would make it so “var f = id;” would require that any assignment to “f” be at least as polymorphic as “a -> a” (“forall (b = a -> a) ref b”, or “ref (forall a . a -> a” if you inline rigid binding). As far as I know, this avoids the same problem the value restriction avoids with different trade-offs. “var f = id; f = not; f(1);” would fail at the assignment from “not” because it isn’t polymorphic enough, rather than at f(1) due to bool !~ number. The difference is the value restriction requires that “f” be monomorphic, while this alternative requires just-as-polymorphic-as, which may or may not be better.

  2. One difficulty with that approach is the need to define a subtype-like relation between type schemes, for example we need to deal with contra-variant type parameters and make sure the “less” or “more” polymorphic decision is reversed.

    Also, for non-function types such as `var arr = []` (which would be inferred to have type `forall a. [a]`) the user will get an error when trying to assign a monomorphic type `arr = [1,2]` instead of having the compiler infer that the intended type is `[Number]`. I could have a rule that doesn’t use value restrictions specifically for abstractions, but does use it for the other “expansive” syntaxes, but then I end up implementing both value restriction and the other idea.

    I *do* have polymorphic row fields (“methods”) and indeed unification is complicated there. I’ve decided to take a “hacky” simple approach requiring both type schemes to have the same number of quantified type variables, and then unifying their instantiations – this simply a kind of alpha-equivalence (if I remember correctly). That part of the type system is the one I’m least comfortable with.

    1. Something nice about MLF is that you don’t need to worry about variance (except when printing out types, and only if you want to – `forall (a = forall b . b -> b) r . a -> r` could be rewritten as `(forall a . a -> a) -> r` – unshared rigid bindings can be inlined in the contravariant position, if I remember correctly – but this is entirely optional). The downside being that MLF is otherwise rather complicated.

      I see your point about `var arr = []`. The other idea would require user type annotations for variables when a monomorphic version is desired.

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s