Restricting equality to be less polymorphic than it is

[nikswamy]

We should implement something like this:

//in prims.fst
assume type HasEq: Type -> GTot Type0
assume _: HasEq int
assume _: HasEq bool
val (=) : #a:Type{HasEq a} -> a -> a -> Tot bool

//programmer writes t
type t =
| MkT : int -> int -> t
assume _:HasEq t //compiler generated


//programmer writes s
type s (a:Type) =
| MkS : a -> int -> t
assume _:forall a. HasEq a ==> HasEq (s a)


//programmer writes s
type s' =
| MkS' : (int -> Tot int) -> s'
//compiler generates no assumptions


//programmer write sint
new type sint
//compiler generates no assumptions

[msprotz]

Seems like basic type classes. JK reported a problem where polymorphic equality of bigints doesn't work; can we do something like:

assume val HasEq: a:Type -> (f: a -> a -> bool) -> GTot Type0
val (=) : #a:Type{HasEq f a} -> x:a -> y:a -> Tot (z:bool{z = f x y})

// programmer-defined type
type s = ... something custom ...
let cmp_s x y =
  ... custom comparison function ...
assume _:HasEq s cmp_s

So that the programmer can not only specify which types are comparable, but also specify a comparison function.

[aseemr]

We would also need a ghost version of op =, that allows logical reasoning about equality of types excluded by HasEq (such as arrows).

[catalin-hritcu]

If there was a #needs-metatheory tag this would be a great candidate. Type theory and a very fuzzy notion of equality don't really mix.

[catalin-hritcu]

@aseemr You might be talking about ==, F*'s strangely heterogenous equality?

[nikswamy]

@msprotz : For the record, as per our discussion, HasEq f is even trickier, since we would need f to coincide with the language's logical notion of equality. We agreed on my original post.

[aseemr]

The design of this feature is here: https://github.com/FStarLang/FStar/wiki/Deriving-hasEq-predicate-for-inductive-types,-and-types-of-equalities-in-F*. Comments and suggestions are most welcome.

I can pass the F* universe regressions (in has_eq_impl branch). Issue project-everest/mitls-fstar#70 tracks the port of mitls to this change.

[ad-l]

I'm late to the party but what is the current status of this?

[aseemr]

@ad-l, as of few days back, F* universe regressions passed with this feature. Making it work for mitls needs some more work. I am hoping to get back to it later this week or early next week.

[aseemr]

This has been merged to the master branch.