Hi.
> Thanks Carlos. I wish I could say thank you for clarifying, but I'm
> afraid this is as muddled as all the comments on the two proposals.
>
> I don't want to go over it again. I just want to say that my
> suggestion earlier in the thread is fundamentally different.
>
>> Global instance scope is not ok either: instances should be modular.
> I just plain disagree. Fundamentally.
Global instance scope is not required for principal typing: a
principal type is (just) a type of an expression in a given typing
context that has all other types of this expression in that typing
context as instances.
(Also: instance modularity is not the central issue.)
>>> Wadler & Blott's 1988 paper last paragraph had already explained:
"But
>>> there is no principal type! "
>> There is always a principal type, for every expression.
>> Of course the type depends on the context where the expression
occurs.
> Then it's not a _principal_ type for the expression, it's just a local
type.
> http://foldoc.org/principal
A type system has the principal type property if, given a
term and a typing context, there exists a type for this term in this
typing context such that all other types for this term in this typing
context are an instance of this type.
> We arrive at the principal type by unifying the principal types of
> the sub-expressions, down to the principal types of each atom. W&B
> are pointing out that without global scope for instances, typing
> cannot assign a principal type to each method. (They left that as an
> open problem at the end of the paper. Haskell has resolved that
> problem by making all instances global. Changing Haskell to modular
> instances would be a breakage. Fundamentally.)
>
> Under my suggestion, we can assign a (global) principal type to each
> method -- indeed you must, by giving a signature very similar to a
> class declaration; and that distinguishes overloaded functions from
> parametric polymorphic functions.
A principal type theorem has been proved: see, for example, Theorem 1 in
[1].
Kind regards,
Carlos
[1] Ambiguity and Constrained Polymorphism,
Carlos Camarão, Lucília Figueiredo, Rodrigo Ribeiro,
Science of Computer Programming 124(1), 1--19, August 2016.
On Mon, 8 Oct 2018 at 20:03, Anthony Clayden <anthony_clay...@clear.net.nz>
wrote:
> On Tue, 9 Oct 2018 at 7:30 AM, <cama...@dcc.ufmg.br> wrote:
>
> Thanks Carlos. I wish I could say thank you for clarifying, but I'm afraid
> this is as muddled as all the comments on the two proposals.
>
> I don't want to go over it again. I just want to say that my suggestion
> earlier in the thread is fundamentally different.
>
> Em 2018-10-08 06:21, Anthony Clayden escreveu:
>> > On Mon, 8 Oct 2018 at 8:41 PM, Simon Peyton Jones wrote:
>> >
>
>
> Strange: Simon's message has not appeared on the forum (he did send to
> it). I've quoted it in full in my reply, but did break it into separate
> pieces.
>
>
>>
>> Global instance scope is not ok either: instances should be modular.
>
>
> I just plain disagree. Fundamentally.
>
>
>> >
>> > Wadler & Blott's 1988 paper last paragraph had already explained: "But
>> > there is no principal type! "
>>
>> There is always a principal type, for every expression.
>> Of course the type depends on the context where the expression occurs.
>
>
> Then it's not a _principal_ type for the expression, it's just a local
> type.
> http://foldoc.org/principal
>
> We arrive at the principal type by unifying the principal types of the
> sub-expressions, down to the principal types of each atom. W&B are pointing
> out that without global scope for instances, typing cannot assign a
> principal type to each method. (They left that as an open problem at the
> end of the paper. Haskell has resolved that problem by making all instances
> global. Changing Haskell to modular instances would be a
> breakage. Fundamentally.)
>
> Under my suggestion, we can assign a (global) principal type to each
> method -- indeed you must, by giving a signature very similar to a class
> declaration; and that distinguishes overloaded functions from parametric
> polymorphic functions.
>
>
> AntC
> _______________________________________________
> Haskell-prime mailing list
> Haskell-prime@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime
>
_______________________________________________
Haskell-prime mailing list
Haskell-prime@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime
