Implicit lambda arguments

[edwinb]

Issue by clayrat Sunday Jul 28, 2019 at 00:28 GMT Originally opened as https://github.com/edwinb/Idris2-boot/issues/56

---

(This is more of a feature request, but it's been a long-standing stumbling block for me in Idris 1, and I hope it's fairly uncontroversial)

Steps to Reproduce

module Temp

import Data.Vect 

All : (a : i -> Type) -> Type
All a {i} = {j : i} -> a j

Vect' : Type -> Nat -> Type
Vect' = flip Vect 

infixr 1 :->
(:->) : (a, b : i -> Type) -> (i -> Type)
(:->) a b i = a i -> b i

showAll : All (Vect' Integer :-> Vect' String)
showAll = map show

justShowAll : Maybe (All (Vect' Integer :-> Vect' String))
justShowAll = Just ?hole

Expected Behavior

justShowAll = Just $ \{j} => map show

Observed Behavior

There doesn't seem to be a way to introduce the implicit to finish filling the hole.

[edwinb]

Comment by edwinb Sunday Jul 28, 2019 at 12:17 GMT

---

Internally, these exist, but there's no syntax yet. There is a possible complication - implicits might appear in a different order than the lambdas, so perhaps there needs to be a way to indicate which implicit argument you mean (in much the same way as you write {n = foo} in a function call) and so it might need to be able to handle lambdas appearing in a different order than in the type.

On the other hand, a simple approach would be to say that if you have an implicit lambda, it needs to be "the next one".

Anyway, all of that is why I've never implemented it. But it would be nice to have.

[edwinb]

Comment by clayrat Sunday Jul 28, 2019 at 13:31 GMT

---

Yeah I think going for a simpler solution and assuming a fixed order might be good enough for a start. This is what happens when matching on auto implicits already anyway, right?

[clayrat]

What about simply reusing the = syntax: \{x=y} => ..., and have \{x=x} ~ \{x}?

[ShinKage]

I've issued a PR https://github.com/idris-lang/Idris2/pull/907 for this feature. However I've only implemented the syntax without the binding rename (i.e. \{x=y}). Correct me if I'm wrong, but the only example I've managed to produce where the rename would be somewhat useful is this:

the ({x : Nat} -> {y : String} -> ()) (\{y, x} => ()) {y="str",x=2}

here you can see that if we explicitly type the lambda with other names for the arguments than we have to follow the names in the typing declaration rather than the names used in the lambda itself, but having to explicitly type the lambda expression does not defeat the purpose of using a lambda expression in the first place?

Furthermore, if we extend the example provided in the original issue to a type with two implicits:

All : (a : i -> j -> Type) -> Type
All a {i} {j} = {x : i} -> {y : j} -> a x y

Matrix : Type -> Nat -> Nat -> Type
Matrix a n m = Vect n (Vect m a)

infixr 1 :->
(:->) : (a, b : i -> j -> Type) -> (i -> j -> Type)
(:->) a b i j = a i j -> b i j

justShowAll : Maybe (All (Matrix Integer :-> Matrix String))
justShowAll = Just (\{x}, {y} => ?hole)

then even if we used new names, the compiler unifies the implicits correctly and provide this result for ?hole:

   x : Nat
   y : Nat
------------------------------
hole : Vect x (Vect y Integer) -> Vect x (Vect y String)

[ShinKage]

After further discussion with other contributors, I'm somewhat retracting my previous comment. We should have implicit lambda arguments however the syntax must be consistent across the language, thus since braces are already in use for named arguments both in LHS of definition clauses and for named application, they must also be used for named arguments in lambda expressions. Nonetheless, we also have positional syntax for explicit and auto-implicit arguments, therefore I argue we should adopt a new non-overlapping syntax for positional implicit arguments (like @{x} for auto-implicits) that is consistent from LHS to lambdas to applications so we can unify the syntax.

For implementation purpose, positional implicit arguments for lambda are already sort of there, and https://github.com/idris-lang/Idris2/pull/907 could be immediately modified with the syntax of choice. However for named implicits some elaboration changes are required and should be framed in the context of the unified syntax.

[ShinKage]

Here an example of what I'm proposing:

takesImpl : ({i : a} -> {j : b} -> F i j) -> ()
f : (i : a) -> F i j
g : (j : b) -> F i j

callImpl0 : ()
callImpl0 = takesImpl $ \{i} => f i -- should work, i : a

callImpl1 : ()
callImpl1 = takesImpl $ \{j} => g j -- should work, j : b

callImpl2 : ()
callImpl2 = takesImpl $ \{j} => f j -- does not work, j : b, it's named, not positional

-- new syntax for positional argument, whatever it may be (here I'm using a syntax similar to @{} for autoimplicits)
callImpl3 : ()
callImpl3 = takesImpl $ \${x} => f x -- works with x : a

callImpl4 : ()
callImpl4 = takesImpl $ \${j} => g j -- does not work, j : a

[clayrat]

Yeah, this is why I suggested the \{i=j} renaming syntax. It's kind of orthogonal to the positionality but solves a similar issue.

[ohad]

So this issue has been opened just over 3 years ago, and it's stuck 'only' on syntax. We currently have the open proposal and discussion to revamp the named-application syntax #1181, and a related one about infix operators #2400. These are quite subtle, and #1181 is more than 1-year old. I worry that in this case the perfect is the enemy of the good.

In order to make some progress: Perhaps we can adopt the most conservative part of the proposal: binding in anonymous functions is strictly positional in the first instance, with implicit arguments bound as names in braces. So:

g : (forall a. Bar => {foo : Nat} -> Bool -> (str : String) -> {gnu : List a} -> Char) -> Unit

allowed : Unit
allowed = g $ \{a=type, foo}, bool, str', {gnu} => 'a'
disallowed : List Unit
disallowed = 
  [ g $ \{foo, a=type}, bool, str', {gnu} => 'a'   -- disallowed for the moment, foo should appear after the implicit a
  , g $ \{a=type, foo, gnu}, bool, str' => 'a'     -- disallowed for the moment, gnu should appear after the string
  , \{a=type, foo, str}, bool, {gnu} => 'a'        -- disallowed for the moment, named explicit str should appear after bool
  ]

Hopefully at a later time, someone will muster the energy to shepherd #1181 to completion and we'll have the perfect syntax!

[gallais]

allowed = g $ \{a=type, foo}, bool, str', {gnu} => 'a'

This is already allowing a "named" syntax {a=type} which will IMO inevitably lead to confused users who will make a natural parallel with the application syntax and won't understand why they behave differently.

I'd rather we introduced the least amount of syntax possible so that:

1. we don't paint ourselves into a corner
2. we don't risk confusing people

So purely positional argument: \{type} => is to {0 a : Type} -> as \type => is to (0 a : Type).

[Russoul]

One year has passed, I barely remember the proposal I wrote myself 😆. I agree with Guillaume, AFAIK, purely positional syntax is the way Agda does it as well, it's always nice to keep the syntax close to a neighbouring language, as long as the syntax covers the indented behaviour.

One thing I worry about is that named syntax has been used extensively in many projects (Frex, Idris2-LSP, etc.). Could be a headache for maintainers of the respective projects...

Edwin said in the last "new-core" meeting that he intended to simplify the application syntax in the new Idris2 as well. I think Edwin's view on how syntax would look like in the new Idris matches that of Guillaume's in the comment above.

Also, by adopting positional syntax now as a first approximation of the "perfect syntax" we take a step back in regard to named syntax. We are essentially throwing it away for the foreseeable future, AFAIU (if we were to implement Guillaume's version)?