[Haskell-cafe] Impossible types [was [Haskell-prime]: A question about run-time errors when class members are undefined]

[Anthony Clayden]

Transferring from
https://mail.haskell.org/pipermail/haskell-prime/2018-October/004396.html

On Sat, 13 Oct 2018 at 4:04 AM, <camarao at dcc.ufmg.br> wrote:

>
>        Consider for example:
>
>        class F a b where f:: a → b
>        class X a   where x:: a
>        fx = f x
>
>        The type of fx, (F a b, X a) ⇒ b, should not be ambiguous: in
>        distinct contexts, fx can have distinct types (if ambiguity, and
>        'improvement', are as defined below).


[See the -prime message for the "defined below".]


I'm just not seeing why you think any Haskell should accept that. What
value could inhabit `fx` except bottom?

And indeed no Haskell does accept it, not even GHC with all sorts of nasty
extensions switched on, including `AllowAmbiguousTypes`.

GHC will accept class `F` with a Functional Dependency `b -> a`, but still
I can't 'poke' any value into the `x` argument to `f` in the equation for
`fx`.


Note: agreeing with this view can lead to far-reaching consequences, e.g.
> support of
>        overloaded record fields [1,Section 7], ...


There are other ways to support overloaded/duplicate record fields, without
doing this much violence to the type system. Look at the `HasField` class
using Functional Dependencies, in Adam Gundry's work.


polymonads [2] etc.
>

Note that's from a Trac ticket asking for 'dysfunctional' Functional
Dependencies. There's a long discussion from the type-inference brains
trust coming to no discernable conclusion as to whether it's broken type
safety. (Catching incoherence in the Core lint typecheck is not a good
look.)

a) You've not shown any detailed working of how your proposal gives the
type improvement required
   without also descending into incoherence.

b) The combination of Functional Dependencies+Overlapping
Instances+Undecidable Instances might be able to cover just enough,
   but not too much of the requirements (which were never made clear).
   See my worked examples on that ticket -- some of which are really quite
scary.
   See some of Oleg's work on his ftp site with multi-directional FunDeps
and overlaps to achieve injectivity.
   To try to tame the scariness while still supporting enough power, see
the suggestion here
https://ghc.haskell.org/trac/ghc/ticket/15632



>        Further examples can be discussed


I have yet to see a convincing use case (from the very lengthy discussions)
which couldn't be handled already in GHC. I agree the combination of
extensions in GHC (including its bogus consistency check/Trac #10675) can
give alarming surprises; but they don't quite break type safety.



but this example conveys the
>        main idea that ambiguity should be changed; unlike the example
>        of (show . read), no type annotation can avoid ambiguity of
>        polymorphic fx in current Haskell.


Since `fx` is not accepted in current Haskell, whether you can put a type
annotation seems beside the point.


AntC

[1]  Optional Type Classes for Haskell,
      Rodrigo Ribeiro, Carlos Camarão, Lucília Figueiredo, Cristiano
Vasconcellos,
      SBLP'2016 (20th Brazilian Symposium on Programming Languages),
      Marília, SP, September 19-23, 2016.

[2]  https://github.com/carlos1camarao/ghc-proposals/blob/d81c1f26298961ac635ce0724bb76164b418866b/expression-ambiguity.rst
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20181014/404ba48f/attachment.html>