If anyone wants to play with this type of type inference, you can find my
implementation of it here:

https://github.com/keean/Compositional-Typing-Inference.git

Keean.


On 21 February 2015 at 12:38, Keean Schupke <[email protected]> wrote:

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