unisonweb / unison

A friendly programming language from the future
https://unison-lang.org
Other
5.78k stars 270 forks source link

Improve the limits of ability composition/inference #4134

Open alvaroc1 opened 1 year ago

alvaroc1 commented 1 year ago

Based on this thread: https://unisonlanguage.slack.com/archives/CLUNF0J5S/p1685653067844909

I am not sure if it's actionable. But making a ticket so it's not lost to the slack short memory. I have ran into this issue twice for different use cases (though both were trying to abstract over elimination of a particular ability).

-- just an example, i want to remove the `Exception` ability
unsafeFn : Nat ->{IO, Exception} Nat
unsafeFn = id

-- eliminating manually, this works!
safeFn : Nat ->{IO} Nat
safeFn = x -> unsafeRun! '(unsafeFn x)

-- my attempt (amongst a few others), type checks
applyEliminator : 
  ('{h, g} b ->{h} b) ->{} -- something like `unsafeRun!`
  (a ->{h, g} b) ->{} 
  (a ->{h} b)
applyEliminator eliminator fn = a -> eliminator '(fn a)

-- but using it doesn't work!
safeFn2 : Nat ->{IO} Nat
safeFn2 = applyEliminator unsafeRun! unsafeFn

Screenshot 2023-06-01 at 2 56 38 PM

when i start replacing some of the generic type params with concrete types, it works

From Stew:

if you change the type of applyEliminator to talk specifically about IO and Exception it works, but I can't make it work with either one being abstract

From Dan:

I doubt you're doing anything wrong, but this is like a worst case scenario for the current ability checker. This kind of higher-order stuff with multiple row variables is not a very tractable problem. We probably need some kind of annotation to help things out, but I'm not exactly sure what would work well.

The second time I ran into this was something like this:

sample.util.runAppWithEffectHandler : 
  '{IO, Exception} (forall a h. '{g, h} a ->{h, IO} a) 
  -> '{g, IO, Exception, Http, Route} () 
  ->{IO, Exception} ()
sample.util.runAppWithEffectHandler initializer app = ...

...

Counter.handleWithRef : Ref IO Nat -> '{g, Counter} a ->{g, IO} a
Counter.handleWithRef countRef effect = ...

...

runAppWithEffectHandler ((do Counter.handleWithRef (IO.ref 0)) : '{IO, Exception} ('{h, Counter} a ->{h, IO} a)) counter
  I found a value  of type:  g, h1
  where I expected to find:  𝕖, g, h, Counter

    108 |   runAppWithEffectHandler ((do Counter.handleWithRef (IO.ref 0)) : '{IO, Exception} ('{h, Counter} a ->{h, IO} a)) counter

    from right here:

      4 |   '{IO, Exception} (forall a h. '{g, h} a ->{h, IO} a)
pchiusano commented 1 year ago

Related #4084