[Haskell-cafe] Impossible types [was [Haskell-prime]: A question about run-time errors when class members are undefined]
Carlos Camarao
carlos.camarao at gmail.com
Tue Oct 23 19:13:26 UTC 2018
> 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?
The type of fx, (F a b, X a) ⇒ b, is a normal, constrained polymorphic
type, in the proposal. When fx is used so that b is instantiated, type
variable 'a' will become unreachable. Satisfiability will then be
tested: if there is a single instance that satisfies the constraints
with the unreachable type variables, these variables will be
instantiated and the constrains removed ("type improvement").
For example:
-----------A.hs-------------------
module A (fx) where
class F a b where f:: a -> b
class X a where x:: a
fx = f x
----------------------------------
----------- M.hs -----------------
module M (inc) where
import A (fx)
instance F Int (Int->Int)
where f = (+)
instance X Int where x = 1
inc = fx
----------------------------------
You cannot define and use fx nowadays in Haskell, even if a functional
dependency is inserted and ambiguous types are allowed, because no
type improvement is used to instantiate unreachable variables, when
unreachable type variables exist. Ok?
> 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`.
I hope things are clearer now.
>> 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,
Of course.
> without doing this much violence to the type system. Look at the
> `HasField` class using Functional Dependencies, in Adam Gundry's work.
There is no violence to the type system, just simplification and clean-up.
>> 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.
I don't know why you wonder about incoherence being a problem.
> 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
Perhaps you could select one or two examples for discussion.
>> 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.
I think any example of use of any MPTC will be able to be handled,
although perhaps differently, with the proposal.
>> 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.
fx is accepted in the proposal, as well as (show . read). I thought it
was a good example because it is small and illustrates that you cannot
accept it and avoid changing the ambiguity rule by just inserting a
type annotation.
Kind regards,
Carlos
PS: I was away and couldn't see e-mails last week.
On Sun, 14 Oct 2018 at 03:31, Anthony Clayden <anthony_clayden at clear.net.nz>
wrote:
> 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
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20181023/95da7efa/attachment.html>
More information about the Haskell-Cafe
mailing list