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