Behavior of inferred effect arguments without val

[s-zanella]

I was surprised to see that giving no val declaration isn't equivalent to giving one without refinements or effects, as illustrated in the example below.

module M

#set-options "--log_types --print_effect_args"

assume new type p: int -> Type0

assume val f: n:int{p n} -> int

//The three declarations below are equivalent and with all of them g fails to typecheck 
//val g: unit -> int
//val g: unit -> ML int
//val g: unit -> ALL int (fun post _ -> forall a h. post a h)

//Inferred type and effect when no declaration is given; with it g typechecks
//val g: unit -> ALL int (fun post _ -> p 0 /\ (forall a h. post a h))

let g () = f 0

This isn't the case with --stratified. It was confusing for me and at least one other person run into this problem when playing with ex1a-safe-read-write.fst in the tutorial.

Is this really the behaviour we want?
If we prefer to have a consistent behaviour, which one to choose?

[nikswamy]

Default effects are slippery. I made an attempt to remove all default effects a while back, but I failed because it seems our code heavily relies on at least Tot being the default effect for any unannotated computation in the PURE monad; likewise for GTot and the GHOST monad.

I am leaning towards establishing that as the official default effects convention.

We're close to having that behavior currently, except we do not properly detect when a computation has a type that has been annotated. For example, should this computation be considered to have an annotated type-and-effect?

match x, y with 
| _, _ -> (e : Lemma P)

I would argue "yes", this computation has been annotated as Lemma P and we shouldn't turn it into the default effect Tot unit at the top-level. Not handling this properly explains the weird behavior currently observed in #517

Happy to discuss further.

[s-zanella]

Thanks for clarifying this.

Shouldn't ML be the default effect of the ALL monad?
From the example above, it appears it isn't.

[nikswamy]

My point was that we have no default effects aside from Tot and GTot.

The fact that t -> s is interpreted as t -> ML s is orthogonal

[s-zanella]

I see. That's exactly the source of my confusion: that t -> s doesn't infer an effect, but is interpreted as t -> ML s.

I guess you don't want to make ML the default effect of ALL, since you are trying to get rid of default effects.
Would it be a good idea to infer an effect instead of using ML when writing t -> s?
More generally, any alternative that makes writing t -> s or nothing behave the same way would clear the confusion.

[nikswamy]

In discussions with @protz, we were considering changing t -> s to mean t -> Tot s.

Perhaps this will clear some of the confusion, given that Tot will be also the default inferred effect for a PURE computation.

That way, the default effect annotation and default inferred effect will coincide.

But, changing t -> s to mean t -> Tot s will break compatibility with ML. Not such a big deal, I suppose. Anyway, this is all still very much up for discussion.

[s-zanella]

That would be a solution, although losing compatibility with OCaml is unfortunate.

Why is it a bad idea to infer an effect instead of using ML when writing t -> s?
Is it because it would break existing code?

[nikswamy]

Well, one main reason the F* implementation is tractable is that we lack effect polymorphism.

What would you infer for the type of

let apply (f:a -> b) (x:a) = f x

Without resorting to our defaults, we'd have to generalize an effect variable. And the cat's out the bag ...

[catalin-hritcu]

But, changing t -> s to mean t -> Tot s will break compatibility with ML. Not such a big deal, I suppose. Anyway, this is all still very much up for discussion.

I'm a big fan of having soundness and purity be the default, so I think this change would be awesome.

I think the only place where ML compatibility actually matters is bootstrapping. But maybe we could have an extra flag there? Or maybe with --lax that doesn't matter anyway?

[catalin-hritcu]

@nikswamy just fixed this