haskell-cafe@haskell.org
[Top] [All Lists]

Re: [Haskell-cafe] type families and type signatures

Subject: Re: [Haskell-cafe] type families and type signatures
From: Manuel M T Chakravarty
Date: Thu, 10 Apr 2008 13:20:55 +1000
Lennart Augustsson:
On Wed, Apr 9, 2008 at 8:53 AM, Martin Sulzmann <martin.sulzmann@xxxxxxxxx > wrote:

Lennart, you said

(It's also pretty easy to fix the problem.)

What do you mean? Easy to fix the type checker, or easy to fix the program by inserting annotations
to guide the type checker?

Martin

I'm referring to the situation where the type inferred by the type checker is illegal for me to put into the program. In our example we can fix this in two ways, by making foo' illegal even when it has no signature, or making foo' legal even when it has a signature.

To make it illegal: If foo' has no type signature, infer a type for foo', insert this type as a signature and type check again. If this fails, foo' is illegal.

That would be possible, but it means we have to do this for all bindings in a program (also all lets bindings etc).

To make it legal: If foo' with a type signature doesn't type check, try to infer a type without a signature. If this succeeds then check that the type that was inferred is alpha-convertible to the original signature. If it is, accept foo'; the signature doesn't add any information.

This harder, if not impossible. What does it mean for two signatures to be "alpha-convertible"? I assume, you intend that given

  type S a = Int

the five signatures

  forall a. S a
  forall b. S b
  forall a b. S (a, b)
  Int
  S Int

are all the "alpha-convertible".  Now, given

  type family F a b
  type instance F Int c = Int

what about

  forall a. F a Int
  forall a. F Int Int
  forall a. F Int a
  forall a b. (a ~ Int) => F a b
  <and so on>

So, I guess, you don't really mean alpha-convertible in its original syntactic sense. We should accept the definition if the inferred and the given signature are in some sense "equivalent". For this "equivalence" to be robust, I am sure we need to define it as follows, where <= is standard type subsumption:

  t1 "equivalent" t2  iff   t1 <= t2 and t2 <= t1

However, the fact that we cannot decide type subsumption for ambiguous types is exactly what led us to the original problem. So, nothing has been won.

Summary
~~~~~~~
Trying to make those definitions that are currently only legal *without* a signature also legal when the inferred signature is added (foo' in Ganesh's example) doesn't seem workable. However, to generally reject the same definitions, even if they are presented without a signature, seems workable. It does require the compiler to compute type annotations, and then, check that it can still accept the annotated program. This makes the process of type checking together with annotating the checked program idempotent, which is nice.

Manuel

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@xxxxxxxxxxx
http://www.haskell.org/mailman/listinfo/haskell-cafe

<Prev in Thread] Current Thread [Next in Thread>