MPTCs and rigid variables

[David House]

class Foo a b | a -> b
instance Foo Int String
bar :: Foo Int b => b
bar = "rargh"

Is there any reason why that shouldn't work? GHC gives one of its
silly "b is a rigid variable" errors (aside: that's a really confusing
error; I'd prefer something like Hugs's "Infered type is not general
enough").

--
-David House, dmhouse@...
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@...
http://www.haskell.org/mailman/listinfo/haskell-cafe

[David House]

On 03/03/07, Bryan Burgers <bryan.burgers@...> wrote:
> As far as I know, you should be defining the type of bar in the class
> declaration for Foo, not in an instance declaration.

I think I over-reduced my problem. Here's a more complex issue that
can't be resolved by moving bar to be a method of the class:

{-# OPTIONS_GHC -fglasgow-exts #-}

class Foo a b | a -> b where
  foo :: Foo b c => a -> Maybe c

instance Foo String () where foo _ = Nothing
instance Foo Int String where foo 4 = Just (); foo _ = Nothing

--
-David House, dmhouse@...
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@...
http://www.haskell.org/mailman/listinfo/haskell-cafe

[C Rodrigues]

>{-# OPTIONS_GHC -fglasgow-exts #-}
>
>class Foo a b | a -> b where
>   foo :: Foo b c => a -> Maybe c
>
>instance Foo String () where foo _ = Nothing
>instance Foo Int String where foo 4 = Just (); foo _ = Nothing
>

There appears to be a type-safe way to use unsafeCoerce# for this:

--------
import qualified GHC.Exts

class Foo a b | a -> b where foo :: a -> FooBox b
data FooBox b = forall c. Foo b c => FooBox (Maybe c)

instance Foo () ()
instance Foo String () where foo _ = FooBox Nothing
instance Foo Int String where foo 4 = FooBox $ Just (); foo _ = FooBox
Nothing

runFoo :: (Foo a b, Foo b c) => a -> Maybe c
runFoo x = case foo x of FooBox x -> GHC.Exts.unsafeCoerce# x
--------

The class constraint check of a,b,c gets moved to the runFoo method instead
of the instance declarations.  Between the body of foo and the call to foo
in runFoo, type 'c' is unknown to the compiler, so we have to encapsulate it
in a FooBox.  The unsafeCoerce# is safe because the type constraint (Foo b
c) that we've placed both on FooBox and on runFoo permits c to have only the
type uniquely specified by b.

We actually could remove the Foo constraint on FooBox, which makes the code
no longer typesafe but it will still work just fine.

_________________________________________________________________
Don’t miss your chance to WIN 10 hours of private jet travel from Microsoft®
Office Live http://clk.atdmt.com/MRT/go/mcrssaub0540002499mrt/direct/01/

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

[David House]

On 03/03/07, C Rodrigues <red5_2@...> wrote:
> class Foo a b | a -> b where foo :: a -> FooBox b
> data FooBox b = forall c. Foo b c => FooBox (Maybe c)

Existential boxes is indeed the method I've used to tackle this in
practice. However, it's kind of annoying, hence my email asking
whether there's a good reason it's not possible. I guess there are no
theoretical limitations, because, as you've just shown, you can hack
your way around it.

--
-David House, dmhouse@...
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@...
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Iavor Diatchki]

Hello,

There is nothing wrong with this program.   I have run into this
problem and I consider it to be a bug/weakness of the type checking
algorithm used by the implementation.

(I also agree with you that the term "rigid variable" is rather
confusing because it is an artifact of the type checking algorithm
used by GHC.)

-Iavor

On 3/3/07, David House <dmhouse@...> wrote:

> class Foo a b | a -> b
> instance Foo Int String
> bar :: Foo Int b => b
> bar = "rargh"
>
> Is there any reason why that shouldn't work? GHC gives one of its
> silly "b is a rigid variable" errors (aside: that's a really confusing
> error; I'd prefer something like Hugs's "Infered type is not general
> enough").
>
> --
> -David House, dmhouse@...
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe@...
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>

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

[Simon Peyton-Jones]

| > class Foo a b | a -> b
| > instance Foo Int String
| > bar :: Foo Int b => b
| > bar = "rargh"

| There is nothing wrong with this program.   I have run into this
| problem and I consider it to be a bug/weakness of the type checking
| algorithm used by the implementation.
|
| (I also agree with you that the term "rigid variable" is rather
| confusing because it is an artifact of the type checking algorithm
| used by GHC.)

Some brief comments

a) I agree there is nothing wrong with this program, BUT it can't be translated into System F.   That's why GHC rejects it.  However, it *can* be translated into System FC (see "System F with type equality coercions", on my home page).  But doing so requires a new implementation of type inference for functional dependencies, and I have not done that yet.

b) While the program is arguably OK, I have yet to see a really convincing application that needs it.  Why not write bar :: String?

c) I really want to get rid of functional dependencies altogether, in favour of associated types.  Thus
        class Foo a where
          type Bar a
        instance Foo Int where
          type Bar Int = String
        bar :: Foo a => Bar a
        bar = "rargh"
This too requires work on type inference, and we're actively working on that.

4.  The "rigid type variable" thing isn't just an implementation question.  What *would* you like the error message to say when you write
        f :: ([a], Int) -> Int
        f (x:xs, y) = x+y
Here we unify 'a' with Int, which is wrong.  What would a nicer error message say?

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

[Tim Chevalier]

On 3/5/07, Simon Peyton-Jones <simonpj@...> wrote:
> 4.  The "rigid type variable" thing isn't just an implementation question.  What *would* you like the error message to say when you write
>         f :: ([a], Int) -> Int
>         f (x:xs, y) = x+y
> Here we unify 'a' with Int, which is wrong.  What would a nicer error message say?
>

IMO, the "rigid type variable" error message is confusing for two
reasons: (1) it doesn't suggest to the user (or at least the
novice-to-intermediate user) what they should do to solve the problem,
and (2) it makes the user feel like they need to go read six papers on
type inference before they can make any progress when all they wanted
to do is add two numbers.

In this particular case, something like "Suggested fix: change 'a' in
the type signature to 'Int'" would be an improvement: it addresses
reason (1), and putting it ahead of the "rigid type variable" part
(e.g., textually highlighting the more newbie-friendly portion of the
error message) addresses reason (2). (I realize that the same error
might occur in cases where the type variable isn't bound by a user
type signature, but it's common enough for users to insert type
signatures when the code isn't compiling that I think it's worth it to
treat that as a special case, even if there isn't a more general way
to improve the error message.)

Cheers,
Kirsten

--
Kirsten Chevalier* chevalier@... *Often in error, never in doubt
"And I have grown with each disappointment through the years" -- Great Big Sea
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@...
http://www.haskell.org/mailman/listinfo/haskell-cafe

[David House]

On 06/03/07, Simon Peyton-Jones <simonpj@...> wrote:
> 4.  The "rigid type variable" thing isn't just an implementation question.  What *would* you like the error message to say when you write
>        f :: ([a], Int) -> Int
>        f (x:xs, y) = x+y
> Here we unify 'a' with Int, which is wrong.  What would a nicer error message say?

"Inferred type was monomorphic but a polymorphic type was given", or
something. Hugs says "Inferred type not as polymorphic as expected",
which is the right kind of area.

--
-David House, dmhouse@...
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@...
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Simon Peyton-Jones]

| > 4.  The "rigid type variable" thing isn't just an implementation question.  What *would* you like the
| error message to say when you write
| >        f :: ([a], Int) -> Int
| >        f (x:xs, y) = x+y
| > Here we unify 'a' with Int, which is wrong.  What would a nicer error message say?
|
| "Inferred type was monomorphic but a polymorphic type was given", or
| something. Hugs says "Inferred type not as polymorphic as expected",
| which is the right kind of area.

Hmm.  But at the moment the type error happens, we are indeed unifying 'a' with Int, and I think it's helpful to say so.  What Hugs does (I think) is to infer the most general type of the untyped fn, and compare with the signature. But in general that gives worse error messages; and when you have higher-rank types you can't ignore the type sig and do inference first.

I'm not against adding "type is too monomorphic" or something like that if you think it'd help, but I'd like to say something about the incompatibility of 'a' and 'Int'.  No?

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

[David House]

On 06/03/07, Simon Peyton-Jones <simonpj@...> wrote:
> I'm not against adding "type is too monomorphic" or something like that if you think it'd help, but I'd like to say something about the incompatibility of 'a' and 'Int'.  No?

Here's a proper draft, then.

Foo.hs:
foo :: [a] -- line 1
foo = "hello" -- line 2

Error message:
Inferred type is not as polymorphic as type signature claims.
  Inferred type: [Char]
  Expected type: [a]
    Provided by the type signature:
      foo :: [a]
    at ~/foo.hs:1
(`a', a polymorphic type variable, could not be unified with `Char', a
monotype.)
In the expression: "hello" at ~/foo.hs:1:8
In the definition of `foo': foo = "hello"

How's that sound?

--
-David House, dmhouse@...
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@...
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Claus Reinke]

> Error message:
> Inferred type is not as polymorphic as type signature claims.
>  Inferred type: [Char]
>  Expected type: [a]
>    Provided by the type signature:
>      foo :: [a]
>    at ~/foo.hs:1
> (`a', a polymorphic type variable, could not be unified with `Char', a
> monotype.)
> In the expression: "hello" at ~/foo.hs:1:8
> In the definition of `foo': foo = "hello"
>
> How's that sound?

too complicated? more explanation isn't always more helpful. the user is confused
at this point, and more information might mean more confusion. compare with

    Hugs> let {foo :: [a];foo = "hello" } in "oops"
    ERROR - Inferred type is not general enough
    *** Expression : foo
    *** Expected type : [a]
    *** Inferred type : [Char]

    Prelude> let {foo :: [a];foo = "hello" } in "oops"
    <interactive>:1:22:
        Couldn't match the rigid variable `a' against `Char'
          `a' is bound by the type signature for `foo'
          Expected type: [a]
          Inferred type: [Char]
        In the definition of `foo': foo = "hello"
        In the definition of `it':
            it = let
                   foo :: [a]
                   foo = "hello"
                 in "oops"

personally, i like the Hugs version best, but the GHC version is consistent
and informative as well. the problem is that GHC refers to a new concept,
rigid variables, whereas Hugs keeps things basic (and even that takes some
getting used to for beginners). rigidness is a useful concept, once you get used
to it. and GHC's message actually contains an explanation of what rigid means
in this context, but that in itself isn't obvious when the user is freshly confused
by that new term (not to mention the rejected program).

perhaps just replacing the line

    `a' is bound by the type signature for `foo'

with

    instantiating `a' with `Char' would conflict with the explicit type signature for `foo'

might help. perhaps a section in the user's guide on the topic "how to interpret
error messages" (Simon Thompson had such a thing for the mysteries of Hugs
messages), and a "dictionary of terms used" (briefly explaining 'rigid' and the like)
would not go amiss, either. these days, they could perhaps be a wiki, growing as
needed, but you'd want to copy snapshots into releases, right into the user's guide.

claus

ps. i was somewhat shocked to read that SPJ wants FDs gone.

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

[Lennart Augustsson]

On Mar 6, 2007, at 22:47 , Claus Reinke wrote:

>
> ps. i was somewhat shocked to read that SPJ wants FDs gone.
>

Why?  Simon has good taste. :)
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@...
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Isaac Dupree]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1


> too complicated? more explanation isn't always more helpful. the user is
> confused
> at this point, and more information might mean more confusion.

That is true, but my experience is that when an error message perplexes
me I need all the suggestions I can get from more error messages.
Sometimes a Hugs error has helped me more than a GHC error, and
sometimes the other way around.  Type inference is complicated and
doesn't know where your mistake is, so it may be best to point out
several views of the problem in case one of them makes sense.

(of course it could also be that I was writing programs that were too
complicated for me to understand, as I was still learning good style in
Haskell :))

Isaac
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.3 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iD8DBQFF7fc7HgcxvIWYTTURArAFAKDGCu6KwtCLen/UBj0FcS7LdKabKgCgknms
deZzzGy0uFDPMoXxJMLPVF4=
=inId
-----END PGP SIGNATURE-----
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@...
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Claus Reinke]

>> ps. i was somewhat shocked to read that SPJ wants FDs gone.
>
> Why?  Simon has good taste. :)

de gustibus non est disputandum ;)

FD have uses and problems and AT have uses and problems. starting anew
with the latter doesn't fix the problems, it just changes their form.

if AT are meant to take over from FD, then either they have fewer uses or
similar problems. the assumption seems to be that AT are somehow equivalent
to FD, as in "any working FD program has an equivalent AT form".

but if the problems can be fixed in the AT form, they can be fixed in the FD
form, and if the problems cannot be fixed in the FD form, they cannot be fixed
in the AT form. in particular, many of the problems with FD are ambiguities in
interpreting interactions with other popular features, such as overlap resolution.
it took half a decade of practical experience to expose such issues for FD, and
i don't see the fact that AT haven't reached that stage yet as any advantage.

there are examples for which the AT form looks nicer than the FD form,
and there are examples for which the AT form is more complicated than
the FD form. about the only half-way convincing non-aesthetic argument
i recall in favour of AT is that their restricted form might help to exclude
problematic programs, but if that is true, imposing equivalent restrictions
on FD should have similar benefits.

i was hoping that the delay on standardising FD meant that we would get
an additional option, with opportunities to gain insights into the issues with
AT, without losing the FD view. after that, the issues common to both FD
and AT ought to be sorted out. only *after* that would there be any point
in chosing one of the two on aestethic grounds, and possibly phasing out
support for the other.

unless i'm missing something, and all this has already happened?-)

claus

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

[apfelmus]

Claus Reinke wrote:
>>> ps. i was somewhat shocked to read that SPJ wants FDs gone.
>>
>> Why?  Simon has good taste. :)
>
> de gustibus non est disputandum ;)
>
> FD have uses and problems and AT have uses and problems. starting anew
> with the latter doesn't fix the problems, it just changes their form.

Well, the choice between FD and AT (and maybe yet undiscovered
alternatives) is entirely a matter of "convenience" as much as
everything related to type inference is. The same goes for type classes
or subtyping: all these can be translated to system F (or FC for FD and
AT) so they don't add abstraction power at run-time. Their only but
important purpose is to auto-infer code.

FD are pretty much type-level programming in a kind of mini-prolog. Of
course, AT are type-level programming as well, but functional in style,
which is arguably more compelling for a functional base language. At
least, I think that FD are somehow ugly.

> in particular, many of the problems with FD are ambiguities in
> interpreting interactions with other popular features, such as overlap
> resolution. it took half a decade of practical experience to expose
> such issues for FD, and i don't see the fact that AT haven't reached
> that stage yet as any advantage.

Quite telling that it took half a decade to shed light on the semantics
of the many FD variants, isn't it? :)

I guess that AT will come with semantics included because it's otherwise
unclear how to implement them. Implementing FD is simply easier as type
inference already is a kind of mini-prolog. Of course, that doesn't
simplify their semantics at all. In a sense, knowing AT is knowing how
much functional in style type inference can be.

Regards,
apfelmus

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

[mm-10]

F, FD, FC, AT, SPJ ;) WTH does it mean?

On Wed, Mar 07, 2007 at 10:12:11AM +0100, apfelmus@... wrote:

> Claus Reinke wrote:
> >>> ps. i was somewhat shocked to read that SPJ wants FDs gone.
> >>
> >> Why?  Simon has good taste. :)
> >
> > de gustibus non est disputandum ;)
> >
> > FD have uses and problems and AT have uses and problems. starting anew
> > with the latter doesn't fix the problems, it just changes their form.
>
> Well, the choice between FD and AT (and maybe yet undiscovered
> alternatives) is entirely a matter of "convenience" as much as
> everything related to type inference is. The same goes for type classes
> or subtyping: all these can be translated to system F (or FC for FD and
> AT) so they don't add abstraction power at run-time. Their only but
> important purpose is to auto-infer code.
>
> FD are pretty much type-level programming in a kind of mini-prolog. Of
> course, AT are type-level programming as well, but functional in style,
> which is arguably more compelling for a functional base language. At
> least, I think that FD are somehow ugly.
>
> > in particular, many of the problems with FD are ambiguities in
> > interpreting interactions with other popular features, such as overlap
> > resolution. it took half a decade of practical experience to expose
> > such issues for FD, and i don't see the fact that AT haven't reached
> > that stage yet as any advantage.
>
> Quite telling that it took half a decade to shed light on the semantics
> of the many FD variants, isn't it? :)
>
> I guess that AT will come with semantics included because it's otherwise
> unclear how to implement them. Implementing FD is simply easier as type
> inference already is a kind of mini-prolog. Of course, that doesn't
> simplify their semantics at all. In a sense, knowing AT is knowing how
> much functional in style type inference can be.
>
> Regards,
> apfelmus
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe@...
> http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[Claus Reinke]

hi mm (?-),

> F, FD, FC, AT, SPJ ;) WTH does it mean?

sorry about this acronymitis :) there was a lengthy debate about some of these
things in the context of haskell' a year or so ago, and i just fell back into the mood,
forgetting to explain my acronyms before using them again

    F: System F, polymorphic lambda-calculi due to Girard
    FC: System F, extended with equality coercions,
    FD: functional dependencies, as in Hugs/GHC
    CHR: constraint-handling rules, used for operational semantics of MPTC with FD
    AT: associated types, as in GHC
    SPJ: advanced haskell processor, theory and practice
    MPTC: multi-parameter type (constructor) classes, as in Hugs/GHC/?

    ACRONYM: abbreviations can relatively often nix your message

for relevant publications see Mark Jones on FD,MPTC origins, Simon Peyton
Jones, Martin Sulzmann, Manuel Chakravarty on more recent work on FC,AT,
FD,CHR. also check the bibliography section at haskell.org, in particular the
part on type systems:

http://www.haskell.org/haskellwiki/Research_papers/Type_systems

hth
claus

hth: hope this helps

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

[Iavor Diatchki]

Hello,

On 3/7/07, Claus Reinke <claus.reinke@...> wrote:
>     AT: associated types, as in GHC

ATs are not in any of the official GHC releases... Are they in the CVS head?

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