[nem-en] Clarification on type-inference rules #2

[Gerard Murphy]

Michal,

To cut a long story short, I agree with your diagnosis and overall
conclusion completely!

I'm looking forward to the next version of the compiler...

...in the meantime, I'll get on with those tutorial exercises.

BTW: I'm hoping to publish a small open-source testing utility on my website
before too long, and yes, I want to write this utility in Nermerle. Keep
your eyes peeled in a month's time or so.

Thanks for what has been a very insightful discussion. :-)

Cheers,

Gerard


Gerard Murphy, www.sageserpent.com




> -----Original Message-----
> From: devel-en-bounces at nemerle.org [mailto:devel-en-bounces at nemerle.org]
> On Behalf Of Michal Moskal
> Sent: 14 November 2005 12:44
> To: devel-en at nemerle.org
> Subject: Re: [nem-en] Clarification on type-inference rules #2
> 
> On 11/13/05, Gerard Murphy <g.j.murphy at sageserpent.com> wrote:
> > Michal, Kamil
> >
> > I thought I'd start a new thread on this, as it's getting quite hard to
> read
> > through all the levels of replies.
> >
> > I've read all of your messages so far: I get the impression that I have
> > persuaded you two to consider implementing support for non-directed,
> > inferred polymorphic types in local definitions, specifically for the
> '[]'
> > and 'array[]' expressions.
> >
> > After some reflection, I'm having second thoughts on this - I think my
> > orginal advice was seriously wrong.
> >
> > I confess that my first impulse on this was to look at OCAML, where []
> is
> > completely polymorphic and of type list 'a. Even if I write code like...
> >
> > let troublesome = ref [];;
> >
> > troublesome <- [ "Gotcha" ];;
> >
> > ... in an interactive session with the OCAML interpreter, it will
> reunify
> > the type of 'troublesome' from ref list 'a to ref list string. This is
> valid
> > because the original value of [] is simply forgotten, so it remains
> validly
> > typed as list 'a.
> 
> This is not exactly how it works in OCaml. When you write let x = ref
> [], you get x : '_a list ref, note the '_'. This means that the value
> is not polymorphic, it just doesn't have a type yet. This is also how
> it should work in our interative interpreter, but unfortunately it
> doesn't support passing type variables between expressions yet.
> However in the regular code you can always do:
> 
>   mutable l = [];
>   l = [ "gotacha" ];
> 
> with essentially the same effects.
> 
> Still [] has a proper (forall 'a. 'a list) polymorphic type in OCaml.
> In Nemerle [] is a shortcut for "list.Nil ()", where list.Nil has type
> (forall 'a. void -> list['a]), so the application results here in a
> free, unquantified type variable, that is going to be unified later.
> 
> [snip]
> > A naïve implementation would emit these interfaces for each site in the
> code
> > where [] or array[] is seen.
> 
> You cannot do that in each and every place where [] is used, because
> you wouldn't be able to do 1 :: [] and the like. This is only needed
> later in code generation, where the proper type of [] cannot be found.
> 
> The problem is that we would need to analyse types to find such cases.
> Such occurchecks are possibly expensive, though I guess they are
> unavoidable anyway (we now use stack-height restriction).
> 
> > Note that I'm still thinking here along the lines that [] is independent
> of
> > any particular substitution of 'a in list 'a, just as it is in OCAML - I
> > know that's not how it works in Nermele at the moment; each [] belongs
> to
> > some specific substitution: list <something> . I'm assuming for the sake
> of
> > argument that you might change that behaviour.
> 
> We cannot change this physically. The tail of the list['a] needs to
> have type list['a] which is impossible for any single Nil type to
> fullfil, so we need Nil['a].
> 
> [snip]
> > If I was doing this in C++, Java 2 or C# or Ada or Eiffel or whatever, I
> > would have accepted that polymorphic types are directed and would have
> > supplied some arbitrary type to substitute for the free type variable...
> >
> > array[]: int, or array[]: string, or array[]: IBogus
> >
> > This is bit nasty when I think of the dizzying heights of OCAML, but I
> do
> > this every day in C++ without batting an eyelid:-
> >
> > new std::vector<StubTypeForTesting>()
> 
> We wanted to avoid this kind of stuff. But here we have a choice of
> requiring the user to supply the type, or giving the function some
> unexpected compiler generated type. As the later can be source of bugs
> and the former cannot, I would go with the former.
> 
> > So my point is to have the compiler reject any use of [] or array[] that
> > leaves the expression type is being polymorphic, unless it occurs in a
> > directed context, i.e. where the type variables are supplied by an
> enclosing
> > generic construct. I'm quite happy to accept this as a necessary evil.
> 
> So I guess we agree here :-)
> 
> > BTW: doesn't anybody else have any thoughts on this? Again, are there
> any
> > readers from the F# or SML.NET communities?
> 
> I believe they do not support F-bounded polymorphism, which makes type
> cyclic here. But possibly they also use some different strategies of
> compilation.
> 
> [snip]
> > I am assuming here that the type inference mechanism won't do an exact
> > unification of System.Object with the polymorphic type list 'a: rather
> it
> > will recognize that System.Object is a superclass of list 'a and use the
> > latter as the most general unifier, allowing an upcast in the generated
> > code.
> 
> Yes it will.
> 
> >
> > Similarly, I assume that System.Array unifies with array 'a to make
> array
> > 'a: again, an upcast would take place in the generated code.
> 
> Again, right :-)
> 
> What we need to do here anyway, is to detect this unfortunate
> IComparable case and signal a better error message...
> 
> --
>    Michal Moskal,
>    http://nemerle.org/~malekith/
> 
> _______________________________________________
> https://nemerle.org/mailman/listinfo/devel-en