On 21 February 2015 at 12:21, William ML Leslie <
[email protected]> wrote:

> On 21 February 2015 at 23:11, Matt Oliveri <[email protected]> wrote:
>
>> I keep forgetting to ask, Keean, how does your proposal handle
>> William's choose_one example?
>>
>
> ​There are probably better pathological cases​ for this model - such as
> two uses, with a different number of parameters given.
>

f g x y = (g x, g x y)

This would not be allowed due to 'g' being monomorphic.

f x y = (g x, g x y)

Would be allowed as you allow top level intersections of the implicit
types, for example:

f :: {g :: fn 'a -> 'd, g :: fn 'a 'b -> 'c} -> fn 'a 'b -> ('d, 'c)

which you could write:

f :: {g :: fn 'a -> 'd /\ fn 'a 'b -> 'c} -> fn 'a 'b -> ('d, 'c)

if you prefer, but as intersections can only occur at the top level, you
don't need to cope with them in unification, so it does not have the
problem of full intersection type systems.

and you treat each "g" as a different instantiation of the polymorphic
function 'g'


I have been working this way a while now, and I guess I didnt realise how
much my reasoning was being influenced by this view of typing. I don't
think I was suggesting BitC should adopt this system, so I guess what I
have realised is that this may be too much of a change in direction.

However, I ca directly do this in my own type inference code which already
works like this, and have an elegant handling of arity which only relies on
a simple subtyping relation.


Keean.



Keean.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev

Reply via email to