Auto Implicit Return Values

[michaelmesser]

I am looking for a way to implicitly return a value from a function.

Say I have the function f : X -> Y. But instead of just returning Y, I was hoping for some way to introduce a proof about the returned value. For example, some way to introduce a proof P y into the ... in let y = f x in .... The proof would need to be available to auto.

My proposed way of achieving that is the following. I'm not certain if this is the right approach yet and would be interested in other methods to achieve the same effect.

data Implicit : (a : Type) -> (a -> Type) -> Type where
    MkImplicit : (x : a) -> (0 _ : p x) -> Implicit a p

f : X -> Implicit Y P

The compiler would implicitly convert the following:

1. Implicit a p to (x : a) introducing p x into the local scope
2. (x : a) to Implicit a p if p x can be found by auto
3. Implicit a p to Implicit a q by combining 1 and 2
4. The rules should be recursively applied to handle nested Implicits

I have no idea how easy or hard that would be to implement or even if this feature is a good idea. I assume it would be somewhat similar to Delay and Force.

The use case I have in mind is emulating weird behaviors of TypeScript such as implicit upcasting. But I imagine there are other use cases as well.

This can be somewhat emulated with a weird version of >>= but it is less than ideal.
It probably could also be emulated with implicit conversions from Idris 1.

Another use of this feature would be improvements to implicit arguments.

function : Implicit JSVal (IsA HTMLElement) -> ...

is cleaner than

function : (x : JSVal) -> {auto 0 _ : IsA HTMLElement x} -> ...

[gallais]

Variables are already available to auto. So you can just bind
the result in a (pattern-matching) let and that should work.

For instance:

an : (a : Type) -> a => a
an a @{p} = p
 
withAuto : Int
withAuto = let p : Int = 3 in an Int

withAuto computes to 3.

[michaelmesser]

I'm confused. Can you explain how to write f : X -> Implicit Y P? I know that Idris can return an implicit argument, but I want to implicitly return a value in addition to the regular return value.

[andrevidela]

Can you explain how to write f : X -> Implicit Y P?

Yes! Turns out you don't have to! Since your goal seem to be to make values available for auto proofs later in the program, binding the result to a variable name is enough to make it avaiable as an implicit value. That's what @gallais is doing here:

an : (a : Type) -> a => a
an a @{p} = p
                  ┌ Bind the value and make it avaiable as `p`
withAuto : Int ╭──┴──╮
withAuto = let p : Int = 3 
            in an Int -- `p` is available here as an implicit argument

There is an additionnal level of cleverness in that example and that is

(x : JSVal) -> {auto 0 _ : IsA HTMLElement x} -> 

is the same as

(x : JSVal) -> IsA HTMLElement x =>

so that is easier to type.

Additionally, if you want an easier way to write your implicits you can create a custom operator that looks like an arrow, let' say =:>. This will allow you to use =:> whenever you want to use this pattern : (x : val) -> {0 auto prf : f x} -> …

infix 0 =:>

(=:>) : {0 input : Type} -> (input -> Type) -> Type -> Type
(=:>) f t = (x : input) -> f x => t

function : IsA HTMLElement =:> ...

[michaelmesser]

@andrevidela You still haven't answered my question. Can you explain how to write f : X -> Implicit Y P so that let y = f x in ... introduces the proof P y in the .... Note that y is not the proof. P y is a proof a about y.

[andrevidela]

@michaelmesser simply bind the proof to a variable:

f : X -> (Y, P)

let (y, prf) = f x in … 

will make the proof prf avaiable to all auto arguments in …

[stefan-hoeck]

@michaelmesser please also note, that a data type like your Implicit already exists: Data.DPair.Subset in base.

[michaelmesser]

@andrevidela
I know that works. The feature request was to make it so that I would only have to write let y = f x in ....

I spoke with @Russoul about this on Slack and he described this as "sugar for automatic wrapping and unwrapping of dependent pairs". Does that help you understand what I'm asking for?

Also {auto 0 _ : P} -> ... is not the same as P => .... The first one has a multiplicity of zero. The second does not.

[michaelmesser]

@stefan-hoeck I'm aware

[gallais]

Would this work for you? Edit: with comments

prefix 0 #

record Implicit {a : Type} (p : a -> Type) where
  constructor (#)
  value : a
  {auto 0 proof : p value}

data Even : Nat -> Type where
  Zero : Even Z
  SSuc : Even n -> Even (S (S n))

anEven : Implicit Even
anEven = # 2

PPred : Even (S (S n)) -> Even n
PPred (SSuc p) = p

it : a => a
it @{p} = p

half : (n : Nat) -> {auto 0 _ : Even n} -> Nat
half Z = Z
half (S (S n)) = let 0 p = PPred it in S (half n)

anHalfEven : Nat
anHalfEven = let (# n) = anEven in half n

[Russoul]

This is probably what michaelmesser wants, applied to your example, gallais:
(only difference is shown)

anEven : Implicit Even
anEven = 2 -- No explicit constructor application
--anEven = # 2

anHalfEven : Nat
anHalfEven = half anEven -- No explicit deconstruction of `anEven`
--anHalfEven = let (# n) = anEven in half n

Wrapping of values x : a for which there is p x into an Implicit a p is done automatically (like implicit conversion).
Same goes for unwrapping of Implicit a p back into an a with the evidence brought into scope (bound to a let behind the scenes).

[andrevidela]

Technically speaking, for this specific example, it could be possible to implement a custom fromInteger function that returns Implicit Even

[michaelmesser]

Russoul's comment correctly describes what I'm looking for.
andrevidela: Yes, but I want it to be general.
gallais: I did something that achieved a similar result by abusing do notation.

namespace Context
    export
    pure : (fst : type) -> {auto 0 p : pred fst} -> Subset type pred
    pure x {p} = Element x p

    export
    (>>=) : Subset type pred -> ((x : type) -> {auto 0 p : pred x} -> Subset type' pred') -> Subset type' pred'
    (>>=) (Element x _) f = f x

None : a -> Type
None _ = ()

data Even : Nat -> Type where
  Zero : Even Z
  SSuc : Even n -> Even (S (S n))

%hint
PPred : Even (S (S n)) -> Even n
PPred (SSuc p) = p

anEven : Subset Nat Even
anEven = pure 2

half : (n : Nat) -> {auto 0 _ : Even n} -> Nat
half Z = Z
half (S (S n)) = S (half n)

anHalfEven : Subset Nat None
anHalfEven = do
    n <- anEven
    pure $ half n

However, I want to be able to use IO at same time. So I did:

data CT : (m : Type -> Type) -> (a : Type) -> (a -> Type) -> Type where
    MkCT : m (Subset a ps) -> CT m a ps

namespace CT
    export
    pure : Applicative m => (fst : type) -> {auto 0 p : pred fst} -> CT m type pred
    pure x = MkCT (pure (pure x))

    export
    (>>=) : Monad m => CT m type pred -> ((fst : type) -> {auto 0 p : pred fst} -> CT m b qs) -> CT m b qs
    (>>=) (MkCT io) f = MkCT $ do
        Element x _ <- io
        let MkCT z = f x
        z

But I couldn't figure out how to write a HasIO instance and I wanted to avoid a lift function. And it just seemed too complex.

[gallais]

(like implicit conversion)

Implicit conversions are evil.

Hence why I believe this belongs in library land rather than in the compiler
(with the obvious caveat you have to wrap / unwrap but you never need to
explicitly refer to the wrapped or unwrapped proofs).

However, I want to be able to use IO at same time.

Right. The direct-style solution should not have the same problems.

[michaelmesser]

How is an auto implicit return value any more evil than an auto implicit argument? Idris already does automatic Force and Delay? How is this any different?

[gallais]

Implicit arguments are solved by unification which is a principled
mechanism with strong guarantees (e.g. we can make sure that all of
the solutions we generate are unique). Implicit outputs on that basis
would be fine by me but that is not what you are asking for.

In the example I cooked you could return {n : Nat} * Even n and
that would mean that n is solved by unification and Even n is
the only explicit value that is returned. But what you seem to want
is the other way around: explicitly have n and automatically infer
the proof.

Idris already does automatic Force and Delay? How is this any different?

Implicit coercions in general make type-checking hell: when you have types
that don't match-up, it's not an error anymore: it's "what if I add an
implicit coercion here? Could I fix it?". We had to recently remove linearity
subtyping for this type of reason. I hope we can keep laziness & coinductive
thunking implicit but I would not bet on it.

[michaelmesser]

I meant to say auto implicit arguments (which I do not believe are solved by unification).

[andrevidela]

@michaelmesser The current proposal about removing Implicit conversions in the upcoming Scala 3 sums it up pretty well regardless of implementation details https://contributors.scala-lang.org/t/can-we-wean-scala-off-implicit-conversions/4388

Auto implicits do not generate any confusions about existing written programs (at least not more than dependent types and type classes).

[gallais]

Most usages of auto implicits are ill-advised. They're a very dangerous
tool that people use instead of proving that something is (semi)-decidable
because it appears to be magic. The half example I gave is, for instance,
a fairly dreadful use of auto implicits as demonstrated by the fact I had
to use tricks like it : a => a to make it work.

[michaelmesser]

gallais you can avoid using it by using %hint on PPred.

[gallais]

You're still doing arbitrary proof search instead of highlighting the fact
that the computation proceeds by structural induction.

[michaelmesser]

I don't see why that is a problem. I don't want to think about the proofs. I want Idris to figure them out.

[michaelmesser]

@andrevidela

Auto implicits do not generate any confusions about existing written programs

How does auto implicit returns generate confusion about existing written programs? Unless Implicit is used, everything will work the same as before.

Also I'm pretty sure Scala has subclasses and implicit upcasting which is the feature I'm trying to emulate.

[gallais]

I don't want to think about the proofs. I want Idris to figure them out.

It won't (not any time soon at least). What you describe is way closer to
e.g. liquid haskell. Where you have these type of subsets everywhere and
you plug in an SMT solver to see whether you can derive the sort of
entailments you described earlier.

In turn you have to compromise and have a less powerful logic to make that
proof search easier.

[andrevidela]

How does auto implicit returns generate confusion about existing written programs?

imagine the following program:

module Source
myVal : Int
myVal = 3

module Main
main : IO ()
main = printLn myVal

imagine now that you import a library to do arithmetic computation and it has somewhere this function exported:

module Evil
implicit
convert : Int -> String
convert = show

what would your program print? "3" or 3?

Now imagine you are not dealing with numbers but HTML templates, which themselves have values which are implicitly converted. You can't tell what's going on until you print the HTML output, assuming you can. If you can't it may be because of a type error on your part, OR it might because of an implicit conversion not triggering properly because something hasn't been imported/implemented/used correctly. Either way the error is going ot be impossible to report because you cannot tell when a type mismatch happens because of an implicit conversion that fired and shouldn't have, or because it's a legitimate error.
Finally it's not like you can say "its easy, don't import implicit conversion", how are you supposed to know implicit conversions are happening in a module? We treat modules like blackboxes and the most those blackboxes can do is bring into scope some variable names (and instances), having the blackbox have the opportunity to arbitrarily change the meaning of every single statement you write is a recipe for disaster.

Finally you have funny programs like this:

-- Shows the ackerman number for the given input
implicit
ackeman : Nat -> String
…

main : IO ()
main = putStrLn 3

What do you think will happen? What should happen? And most importantly, how would the compiler know what is your intent? Now imagine you put this in a compile-time function, you mistakenly type 3 instead of "3"; now typechecking will take forever and you will end up with the wrong value, but you wouldn't know why or how unless you're able to track back this implicit conversion.

[michaelmesser]

@andrevidela I'm not talking about implicit from Idris 1. I think they should be very rarely used. I mean Implicit as defined by my proposal. I think the idea of implicit Nat to String is wrong. I just want to emulate subtyping.

[michaelmesser]

@andrevidela The key difference between my proposal and general implicit is the following.

f : X -> Y
g : A -> B

implicit evil : Y -> A affects the behavior of g (f x) without f or g opting into that behavior.

However with my proposal Implicit and the rules I listed could never affect how f and g interact. My proposal is no different than Lazy and Force automatically being inserted.

[buzden]

I'm wondering why if we would slightly modify code from the Guillaume's comment above, the behaviour is different:

anHalfEven : Nat
anHalfEven = let x = anEven
             in half x.value

gives

Error: While processing right hand side of anHalfEven. Can't find an implementation for Even (.value x).

.../AutoImplicitUnboxing.idr:27:17--27:29
    |
 27 |              in half x.value
    |                 ^^^^^^^^^^^^

But

anHalfEven : Nat
anHalfEven = let x : Implicit Even
                 x = anEven
             in half x.value

typechecks. Looks like when type-ascripted, x is considered as a local hint, but only in this case.

By the way, @michaelmesser, isn't this closer to what you wanted originally?

[ShinKage]

@buzden See here and here why the two lets have different behaviour. In short, it has to do with case and with elaboration. Moreover, where clauses are just type-ascribed lets.

[michaelmesser]

@buzden The custom >>= works better than that.

anHalfEven : Subset Nat None
anHalfEven = do
    x <- anEven
    pure $ half x

[ShinKage]

IMHO, as @gallais said, implicit conversions are evil. While I agree that it may be useful in some cases to automatically carry around proofs (and the mechanism is already there), I would much prefer to have some explicit annotation that we are matching on a value and a proof, maybe a short one like the (#) in one of the previous comments. I always found the implicit casting of Lazy annotated value, confusing at best and straight painful in some cases, and it should haven't been there in the first place as compiler mechanism (instead of library) IMHO.

[michaelmesser]

@ShinKage Why would auto implicit return values be any more evil than auto implicit arguments?

[ShinKage]

@michaelmesser Oh I think that also the current version of auto-implicit arguments are sort of evil. I would advise against using it in any case where the constructed value is not uniquely determined by it's dependecies (e.g. Refl, but even Elem for List can be problematic if there are duplicate in the List as you have to assume that the auto-search always choose one way of constructing it). Furthermore I think there should be a way to explicitly annotate how to search (e.g. search interface instance or find any valid value or more complex user-provided tactics). They can be abused in ways that are hardly debuggable, as the control is not yours but of the particular algorithm used for resolution, and changes in the algorithm have impact on the compilation itself, even changing the default maximum depth can lead to perfectly fine code not compiling with some strange errors that can mislead newcomers and people not invested in the implementation of auto-implicits. There have been multiples issues and question on proofs over interfaces or nested interfaces where the auto-implicits mechanism lead people to wrong assumptions (you often need to explicitly carry around the interface implementation, which is counterintuitive).
I'm not in principle against some sugar, I like idiom brackets for example, and there is probably a good way of sugaring/desugaring auto-implicits but I don't think using the regular explicit argument syntax is the way to go. How should I reason about an auto-implicit argument when there are multiple valid values in scope that can be passed to?

[michaelmesser]

@ShinKage

How should I reason about an auto-implicit argument when there are multiple valid values in scope that can be passed to?

This is what I had in mind:

If the argument has a multiplicity of zero, just pick one.
If all values of the type are identical (HVect [], (), ...) just pick one. The compiler can determine this by attempting generate definition on (x : a) -> (y : a) -> x === y where a is the type.
If all of the values are structurally identical (deciding between 1 and 1), just pick one.
Otherwise, an error should be thrown.

[ShinKage]

What I'm trying to say is not that you cannot find a reasonable procedure for selecting one value over the others (you can get pretty smart about it, trading compile time speed with writing code time) but that while one may be reasonable, it's not the "correct" one. The current approach, and the reasonable procedure, are not zero-cost abstractions, there may be impact depending on the procedure (unexpected error messages or unexpected results depending on which way the procedure prefers) and there is no way currently of refining the abstraction that isn't just ditching the auto-implicit passing behaviour and explicitly pass around the values.
Also, I don't think is a good idea to just pick one with multiplicity zero. It's true that at runtime it does not matter, but it can still be used at compile time to compute some type index, and currently evaluating stuff at compile time is really costly, so the picked value can wildly interfere with compile time computation.

[michaelmesser]

@ShinKage If users want custom behavior instead of auto they can use default implicit arguments with an elaborator script.

[ShinKage]

@michaelmesser It almost works, because if the elaborator script fails then it always fails to typecheck even if you explicitly provide a valid argument to use instead of the default one.