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

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
4 messages Options
Reply | Threaded
Open this post in threaded view
|

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

AntC

On Sat, 13 Oct 2018 at 4:04 AM, <[hidden email]> 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 



       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.
Reply | Threaded
Open this post in threaded view
|

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

AntC

Second instalment.

On Sat, 13 Oct 2018 at 4:04 AM, <[hidden email]> wrote:
...
       Ambiguity should be a property of an expression, defined as
       follows: if a constraint set C on the constrained type C∪D⇒t of
       an expression has unreachable variables, then satisfiability is
       tested for C (a definition of reachable and unreachable type
       variables is at the end of this message), and:

        - if there is a single unifying substitution of C with the set
          of instances in the current context (module), then C can be
          removed (overloading is resolved) and C∪D⇒t 'improved' to
          D⇒t;

        - otherwise there is a type error: ambiguity if there are two
          or more unifying substitutions of C with the set of instances
          in the current context (module), and unsatisfiability
          otherwise.

   2. Allow instances to be imported (all instances are assumed to be
      exported):

            import M (instance A τ₁ ⋯ τₙ , … )

               specifies that the instance of τ₁ ⋯ τₙ for class A is
               imported from M, in the module where the import clause
               occurs.

       In case of no explicit importation, all instances remain
       imported, as currently in Haskell (in order that well-typed
       programs remain well-typed).

Consider some typical Read instances from the Haskell Prelude

> instance Read a => Read [a]  where ...
> instance Read a => Read (Maybe a)  where ...

Suppose I have `show . read` where the 'piggy in the middle' type is unreachable (by your definition below); but I want it to be taken as `(Maybe [Int])`.

Then I arrange my imports of instances to make visible only ... what?

`(Maybe a)` ? Then how do I read the `[a]`? The only instance in scope is `(Maybe a)`.

`(Maybe [Int])` ? Then how do I decompose the structure to call the overloads for `read` of the list and of the `Int`? Instance `(Maybe a)` is not in scope, neither is `[a]` nor `Int`.

And what if in the same module/same scope I want `show . read` where 'piggy in the middle' is `[Maybe Int]` or `(Maybe [Bool])` ? Then instead of `Read`, I could create a whole swag of specialised classes/methods: ReadMaybeListInt, ReadListMaybeInt, ReadMaybeListBool, ... ? But those could just be regular functions with an explicit signature. Putting an explicit type annotation on each expression seems a whole lot more convenient than mucking around with specialised classes or scope of instances.


Before you answer, consider this very common pattern. It's so common there's a base library operator for it: type-level `==` 

> class TypeEq a a' (b :: Bool)  | a a' -> b
> instance TypeEq a a True
> instance (b ~ False) => TypeEq a a' b

Then an example usage

> instance (TypeEq e e' b, TypeIf b This That) => instance Elem e (Cons e' tail)  where ...

Rubric: `Elem` is searching for type `e` in some type-level heterogeneous list; if found (i.e. `TypeEq` returns `True`), the `TypeIf` despatches to `This`, else to `That`.

It's crucial for `TypeEq` that both instances are in scope in all places.

Ah, but I see the `TypeEq` example does not contain any "unreachable" tyvars by your definition below. In which case your specification is silent as to how type improvement is to behave. (But you claim your approach is instead of FunDeps; then what is to happen with both instances being able to unify with the type of some expression?)

Then do you want to change the spec? This was the experience with the github rounds: the spec kept changing; the examples we'd worked through in earlier rounds then didn't work with the new spec. Therefore the claims were impossible to verify with any certainty.





(Definition: [Reachable and unreachable type variables in constraints]
Consider a constrainted type C∪D⇒τ. A variable a ∈ tv(C) is reachable
from V = tv(τ) if a ∈ V or if a ∈ tv(π) for some π ∈ C such that there
exists b ∈ tv(π) such that b is reachable from V; otherwise it is
unreachable.
For example, in (F a b, X a) ⇒ b, type variable 'a' is reachable from
{ b }, because 'a' occurs in constraint F a b, and b is reachable.
Similarly, if C = (F a b, G b c, X c), then c is reachable from {a}.)



AntC


_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

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

Carlos Camarao
In reply to this post by AntC
> Transferring from 

>> On Sat, 13 Oct 2018 at 4:04 AM, <[hidden email]> 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

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 <[hidden email]> wrote:

On Sat, 13 Oct 2018 at 4:04 AM, <[hidden email]> 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 



       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.

_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

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

AntC
On Wed, 24 Oct 2018 at 8:20 AM, Carlos Camarao <[hidden email]> wrote:

Carlos, the more I dig into your proposal/the more answers you provide, then the more crazy it's getting.

I'll stop after explaining why I say that. I'm absolutely sure I don't want this.

SPJ hasn't amplified his "interesting work" comment. You've not indicated if your papers have been peer reviewed nor who by. So in the absence of any independent corroboration, my judgment is there is nothing of merit worth pursuing further.

GHC's current combo of FunDeps+Overlap+UndecidableInstances has its problems. That's why I'm always willing to look at alternatives. But not this crazy.



>> On Sat, 13 Oct 2018 at 4:04 AM, <[hidden email]> 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.

Wait ... what? Instantiating a type variable changes some other type variable from reachable to unreachable?
I'm already struggling to keep up with your definitions, which are different to GHC's definitions.
Type improvement (i.e. instantiating type variables) is supposed to be monotonic: how can it
a) affect other type variables that weren't even mentioned in the type assignment;
b) have an effect on them opposite of improvement?


Satisfiability will then be tested: if there is a single instance that satisfies the constraints

You mean: a single instance in scope. So it's not just that you think scoped instances are a Good Thing
(I disagree, for reasons of type safety);

You require scoped instances so that there's only one instance visible.

What's worse, there's no way to declare for class F that var a is reached from b, as a way to make sure there's only one suitable instance.

So I think that means for the (show . read) example that I need to hide all of the Prelude instances, except the one I want for piggy in the middle.


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?

I am very Ok with how Haskell works. Its definition of 'unreachable' relates to FunDeps.

You are now trying to explain Haskell using a different definition of 'unreachable'. I think that's bogus.

...

I don't know why you wonder about incoherence being a problem.

I don't know why you think anything you've said shows anything about incoherence.
You've given an example with only one instance. Then it's not going to be incoherent with itself.

(The discussion I elided was about the polymonads example, for which you've given no solution. Are you again going to require there be only one Monad instance in scope? Is that going to be one instance per module, or at a finer grain? A polymonad combines two Monads to return a third; won't that require at least two pairings in scope?)

Coherence is a property of the whole program axiomatisation. I.e. all instances for all classes and constraints.


...

Perhaps you could select one or two examples for discussion.

No, the onus is on you to show you are providing equivalent expressivity to what's long been stable in Haskell (GHC and Hugs).

And then you have to show you're providing something that improves on it/addresses its difficulties. Let's see a detailed working for polymonads. All we have so far is hand-waving.


... ambiguity rule ...

Again, you're using a different definition of "ambiguity", as compared with GHC's `AllowAmbiguousTypes` extension.

No wonder it's so hard to follow what you're claiming.


AntC


_______________________________________________
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.