Haskell-in-Agda: Agda propositions (e.g. `x ≡ y`) versus Haskell predicates (e.g. `(x == y) ≡ True`)

Hello! I have two observations / questions about what should go into the Haskell-in-Agda embedding, i.e. the Haskell.Prelude. Unfortunately, they are not fully well-posed. For lack of a better place, I'm opening an issue.

While they may be discouraged in idiomatic Agda, I find that working with Haskell predicates, e.g. (x == y) ≡ True or elem x xs ≡ True, i.e. functions a → Bool that are combined with ≡ True, works surprisingly well. One important advantage is that they are straightforward to understand for the working Haskell programmer, who knows Bool, but is not familiar with Set l.

For example, the definition of elem is strong enough to make refl prove the following Lemma:

lemma-elem
  : ∀ {{_ : Eq a}} (y x : a) (xs : List a)
  → (elem y (x ∷ xs)) ≡ ((y == x) || (elem y xs))
lemma-elem y x xs = refl

I'm wondering how much support Haskell predicates should get in Haskell.Prelude.

From `Bool` to propositions

I can define a propositional version of list membership with the abbreviation.

_∈_ : ∀ {a : Set} {{_ : Eq a}} → a → List a → Set
x ∈ xs = elem x xs ≡ True

However in order to conclude the equivalent of lemma-elem, I would need the following lemma

||-to-proposition
  : ∀ (b b' : Bool)
  → (b || b') ≡ True
  → (b ≡ True) ⊎ (b' ≡ True)
||-to-proposition True b' refl = inj₁ refl
||-to-proposition False True refl = inj₂ refl

Is this worth adding to Haskell.Law.Bool?

(Of course, I'm somewhat contradicting myself in that I would like to use ⊎ now, the propositional version of the || Haskell function. But it seems to be useful in combination with existentials, where I want to express the existence of some element.)

IsLawfulEq — What about quotient types such as `Data.Map`?

The IsLawfulEq class is helpful and necessary for going from (x == y) ≡ True to x ≡ y.

(The reason for wanting to have x ≡ y is that only the proposition can be used for substitutions in arbitrary contexts.)

However, an IsLawfulEq instance does not exist for quotient types such as Data.Map.Map! 😲 Well, or maybe it should, but that's precisely the question I want to ask.

It is not true that any two Data.Map.Map that are (x == y) ≡ True can be substituted for each other in all contexts (≡) — the Data.Map.showTree function can distinguish them. The problem becomes worse if we implement Data.Map.Map in Haskell-in-Agda rather than postulating its properties, as now the compiler inspects terms. Of course, Data.Map.Map is best though of as an abstract data type, and it is "morally" true that we can substitute. Using the abstract keyword in Agda may also help.

I'm not sure what to do here — postulate Data.Map as a quotient type and look the other way, or go into setoid hell?

Though, to be fair, "setoid hell" is not that bad if we think about in terms of using == explicitly — in plain Haskell, we can't get rid of the proof obligation that functions need to respect == and that substitution for values that are merely Eq.== is limited to those functions. (Maybe a variant of cong?)

It's fine to discuss this here, I've also created an #agda2hs stream on the Agda Zulip for more informal discussions and questions.

Regarding boolean propositions, there are two ways of handling them in agda2hs: either using an ≡ True predicate to turn them into Sets, or use a version of the Dec type that compiles to Haskell's Bool type (which you can do by using a transparent record). In my experience, the former is indeed more intuitive to newcomers but leads to a lot of boilerplate lemmas, while the latter requires a bit more set-up but is much nicer since it keeps the boolean and the proof nicely together. So I think we should either try to push users in that direction or simply support both styles. Also pinging @omelkonian and @flupe to hear what's their opinion on this.

Regarding lawful Eq, I wonder how this is actually solved on the Haskell side. Do they only consider the Extensionality law for functions that are defined using the public interface? It might be worth it to experiment with a generic quotient construction that is postulated. Ideally we would have a version of --cubical that is compatible with UIP so we could get actual computation to hold, but absent that we might expose some rewrite rules for it. The other option is indeed to go into setoid hell, but that would require changing how we define LawfulEq.

or use a version of the Dec type that compiles to Haskell's Bool type

Ah, interesting. 🤔

In my experience, the former is indeed more intuitive to newcomers but leads to a lot of boilerplate lemmas, while the latter requires a bit more set-up but is much nicer since it keeps the boolean and the proof nicely together. So I think we should either try to push users in that direction or simply support both styles.

After some thinking, I believe that "newcomer" is probably not the right word. 🤔 Here is a better phrasing of what I mean: "A style where you write Haskell98 code and use equational reasoning to prove properties that the code has (e.g. following the proof style exemplified in Hutton's book or Gibbon's work). However, instead of doing equational reasoning on paper, you formulate it in Agda, so that you a) prove things about the code that is actually compiled, and b) have your proofs checked for validity by a machine". I think that Haskell98 + a) + b) is a highly useful point in the design space, and a strict improvement over what Haskell/GHC can offer at the moment. For lack of a better term, I'd like to call it Haskell98-in-Agda for now. This style would include Bool, but exclude Dec. I think that this is the style that I'm most interested in right now.

Regarding lawful Eq, I wonder how this is actually solved on the Haskell side. Do they only consider the Extensionality law for functions that are defined using the public interface?

Since Haskell98 cannot reason about itself, this problem is left to the metatheory. There, the argument goes as follows:

Data.Map is an abstract data type, so the functions defined in the corresponding module, such as empty, insert, delete, are the only way to introduce and eliminate values of this type. (In order to prove things with this observation, we actually need to express it in the proof assistant, which amounts to a surjective mapping from the free algebra to the abstract data type.)
Eq.== is considered lawful if it is an equivalence relation, and it is expected that all operations on the abstract data type preserve it. For these reasons, we may as well pretend in the metatheory that == corresponds to ≡. (I'm actually often unsure whether I should write = or == when doing a proof by hand for this reason.) (Note that the evidence for the surjectivity mentioned above likely does not preserve == unless we have some sort of normal form.)

After some thinking, I believe that "newcomer" is probably not the right word.

I'm sorry, I did not want to imply that you are a newcomer, just that I've often seen this style being used by my students when they first start using agda2hs.

As far as I know, Haskell98 does not specify any specific style of reasoning, so any way that we decide to formalize that reasoning in Agda is going to require making some choices. It's not because some previous work on reasoning about Haskell98 on paper adapts a certain style, that this is necessarily the best style to encourage in Agda2Hs too. In particular, when we got experienced Agda programmers to try out agda2hs they expressed a general distaste for and annoyance with code that relies heavily on boolean reasoning.

Also, I think we should be careful to distinguish between equational reasoning (which is a style of proof I think we should definitely support) and specifically relying on boolean equality (which I believe generates more pain in the long term).

This style would include Bool, but exclude Dec. I think that this is the style that I'm most interested in right now.

My argument here is that Dec basically is the same type as Bool, with just some extra proofs attached (which can be erased). We could even define the Bool type in Agda like this:

data Bool (@0 P : Set) : Set where
  True  : @0 P       → Bool P
  False : @0 (P → ⊥) → Bool P

Note that this compiles to precisely the same Bool type in Haskell as the standard definition! However, it forces users to acknowledge the fact that a boolean is (almost) never a plain value, but always reflects the truth or falsity of a certain proposition. Using this definition of Bool instead of the standard one would certainly help with reducing boolean blindness.

Now I am not actually arguing to change the definition of Bool, but just showing that there are different possible styles of verifying Haskell code (in particular, extrinsic and intrinsic) and that they are both equally valid ways to "prove things about the code that is actually compiled" and "have your proofs checked for validity by a machine". Just because we call it Dec instead of Bool does not change anything fundamental.

It's not because some previous work on reasoning about Haskell98 on paper adapts a certain style, that this is necessarily the best style to encourage in Agda2Hs too. In particular, when we got experienced Agda programmers to try out agda2hs they expressed a general distaste for and annoyance with code that relies heavily on boolean reasoning.

It may well be the case that the extrinsic style, i.e. a formal system to express the metatheory of Haskell98, is not necessarily the best option, but what I'm saying is that it's a well-defined and highly useful point in the design space that I would not sideline on the grounds that other options could be better.

The extrinsic style has a few advantages:

It is guaranteed to work. I often find myself wrestling with Agda to get it to accept this substitution or that equality. However, I have confidence that if I take the time to write down a proof on paper about Haskell98, then I will eventually be able to formalize it in Agda somehow. This is less clear for proofs in which the metatheory seeps into the source language — for example, C-c C-c in Agda has occasionally refused to expand pattern matches entangled with @0 even though writing the patterns by hand worked.
It is easier to teach to Haskell programmers with no background in dependent type theory. It's a bit of a sightly more social problem: I would like to introduce formal reasoning into our codebase, and I feel that sticking to Haskell98 as source language is the option where people are less inclined to shoot themselves in the foot. For example, I consider the GHC language extension AllowAmbiguousTypes to be synonymous with "I have shot myself in the foot", and you won't believe how often people use this in Haskell codebases. 😅 As another example, I feel that I can explain the difference between == and = to my colleagues, but trying to explain setoids is not going to go very well.

Also, I think we should be careful to distinguish between equational reasoning (which is a style of proof I think we should definitely support) and specifically relying on boolean equality (which I believe generates more pain in the long term).

Maybe so, but in the extrinsic viewpoint, the source language is plain Haskell98, and assumptions will come in the form "Computation foo x y evaluates to True". Everything else is in the metatheory. So, I think the extrinsic viewpoint doesn't give any freedom on how to think about boolean equality, other than those offered by Haskell98, say returning Just x :: Maybe a instead of True :: Bool.

data Bool (@0 P : Set) : Set

Note that this compiles to precisely the same Bool type in Haskell as the standard definition! However, it forces users to acknowledge the fact that a boolean is (almost) never a plain value, but always reflects the truth or falsity of a certain proposition. Using this definition of Bool instead of the standard one would certainly help with reducing boolean blindness.

I like this type. However, one thing I'm not sure about is this: How general is this type? 🤔 I.e. if I wanted to perform logical operations on it, such as || or &&, I presumably would have to operate on the predicate as well? I have the feeling that the predicate depends on the use case, different Bool have different information which does not combine meaningfully.

To give a specific example: I was trying to prove a statement of the form

x ∈ someList → (isBlue x ⊎ isRed x)

It just so happened that in particular case, someList has the form someList = z :: ys with isBlue z and ∀ y → y ∈ ys → isRed y.

How would I express this in terms of a Bool which also contains a predicate? Somehow, the point is that x ∈ refers to list membership, and I can convert that into a statement about the color of x. I don't quite see how packaging a predicate on list membership with the Bool that comes out of elem will help me packaging a predicate about the color.

agda / agda2hs