[Haskell-cafe] Re: Has anyone looked into adding subtyping to Haskell?

[Jon Harrop]

On Thursday 31 May 2007 17:46:38  Al Falloon wrote:
> I kind of saw the overlapping enumeration case as just a common special
> case of the AST problem.

Theoretically, yes. In practice, this is quite an important distinction 
because enumerations do not suffer from the obfuscated error messages that 
arise when you have polymorphic variants derived from "too much" inference.

> I can't think of a lightweight way to encode overlapping enumerations in
> Haskell. 

I'd like to know if this is possible in Haskell.

> If someone can come up with one, it would probably shed some light on the
> right direction for the AST problem. 

I should emphasise that not everyone agrees with me here. I've noticed that 
Jacques Garrigue uses polymorphic variants in that way (their intended way). 
I have tried several times but I always give up and revert to ordinary 
variants for their simpler error messages. Sometimes I replace the ordinary 
variants with polymorphic variants when the program is complete, but only to 
make me look more intelligent.

Just to clarify what you mean, the following "subst" function substitutes 
variables `Var _ in an expression and OCaml infers that the output expression 
needs no `Var constructor (the type 'b):

# let rec subst vars = function
    | `Int _ as e -> e
    | `Var var -> List.assoc var vars
    | `Add(f, g) -> `Add(subst vars f, subst vars g);;
val subst :
  ('a * ([> `Add of 'b * 'b | `Int of 'c ] as 'b)) list ->
  ([< `Add of 'd * 'd | `Int of 'c | `Var of 'a ] as 'd) -> 'b = <fun>

You can see how inferred sum types can get unwieldy quite quickly.

> The other uses of PV, I hadn't been aware of, but it makes a lot of sense.

Yes. I've found them quite useful in application areas that are better suited 
to more dynamic typing, like GUI and web programming. Polymorphic variants do 
a lot to close the gap there.

Incidentally, I have heard people express concerns that polymorphic variants 
will let more bugs through the static type checker because they are weaker. I 
have never had a run-time problem caused by an unintended inference. My 
problems with polymorphic variants always boil down to the error messages.

For example, forgetting the last "var" in that function allows it to pass type 
checking with a completely different inferred type:

# let rec subst vars = function
    | `Int _ as e -> e
    | `Var var -> List.assoc var vars
    | `Add(f, g) -> `Add(subst vars f, subst g);;
val subst :
  (('b *
    ([> `Add of
          'c * (([< `Add of 'd * 'a | `Int of 'e | `Var of 'b ] as 'd) -> 'c)
      | `Int of 'e ]
     as 'c))
   list as 'a) ->
  'd -> 'c = <fun>

-- 
Dr Jon D Harrop, Flying Frog Consultancy Ltd.
OCaml for Scientists
http://www.ffconsultancy.com/products/ocaml_for_scientists/?e