Observational Equality using levitation

[gelisam]

The idea of adding Observational Equality to Klister came up while discussing #162, so I am creating a separate issue to keep track of it.

Before adding Observational Equality, we would first need to add dependent types, because if two values x and y of type A are observationally-equal, that's represented by a proof of type ObsEq {A} x y, not by the fact that some (==)-like function returns true. The key difference between propositional equality and observational-equality (at least according to this very short intro video) is that the former has the same definition for every type (namely, the only constructor is Refl : x -> PropEq {A} x x), whereas the latter has a different definition for every type. In particular, functions use extentional equality (ExtEq : (forall a. ObsEq {B} (f a) (g a)) -> ObsEq {A -> B} f g).

[gelisam]

I am not sure how dependent types nor observational equality relates to Klister. My first impression is that trying to add those features to the language would spread our efforts too thin, so I would prefer to focus on the aspects of Klister which make it unique.

[gelisam]

@david-christiansen mentions relevant literature:

1. "A Cosmology of Datatypes, Reusability and Dependent Types", by Pierre-Evariste Dagand
2. The Gentle Art of Levitation

They are both about a universe whose constructs describe not only all the data types in the language, but also the universe constructs themselves.

Since observational-equality is defined recursively on all the types in the language, it makes a lot of sense to use a universe, that is, a recursive datatype describing all the types in the language. Furthermore, if we want to be able to describe what it means for two observational-equality proofs to be observationally-equal to each other, we need our universe to include a representation of ObsEq {A} x y. If this A is an universe-inhabitant describing a type, then the universe-inhabitant describing ObsEq {A} x y needs to be able to describe universe-inhabitants. So it makes sense to use one of the special universes described in the linked resources.

[david-christiansen]

I don't think that dependent types or observational type theory are relevant here. I was merely expressing that I'd someday, if I had infinite time, like to take the tech in the Klister elaborator and repurpose it to something a bit like what Epigram 2 would have been - I think that would be a fun project!

[gelisam]

Closing then!