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

Anthony Clayden anthony_clayden at clear.net.nz
Thu Oct 25 05:45:16 UTC 2018


On Wed, 24 Oct 2018 at 8:20 AM, Carlos Camarao <redirect at vodafone.co.nz>
wrote:

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

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

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20181025/52f3e771/attachment.html>


More information about the Haskell-Cafe mailing list