# Is my understanding regarding how to implement Quotient Types correct?

I was trying to understand Quotient Types, and determine if Self-Types can be used to implement them. From a Reddit post,

Here is an example and explanation that may be more familiar to non-mathematicians. You can use a list to represent a set. The list [1,2,3] represents a set and [3,2,1] represents the same set. The problem with this is that you can break the abstraction. We could wrap this in a data type Set and define an Eq instance that makes Set [1,2,3] == Set [3,2,1]. We can write a function sum:

sumSet (Set s) = sum s


and we can write a function first:

firstSet (Set s) = first s


The sumSet function is fine, but the firstSet function is problematic. We have Set [1,2,3] == Set [3,2,1] but firstSet (Set [1,2,3]) != firstSet (Set [3,2,1]). If two values are equal, then those values should behave the same in all respects: if x is equal to y then f x ought to be equal to f y for any function f, otherwise we are breaking the abstraction. Actually, sumSet also breaks the abstraction if you have duplicate elements, but we could say that it's a multiset so that Set [1,1] != Set .

This made a lot of sense to me. If my understanding is right (and I'm not sure it is), a Quotient Type can be implemented by simply having an extra "phantom constructor" on your datatype, which returns an equality instead of a member of the datatype. As in,

data UPair (A : Set) : Set where
upair : (a : A) -> (b : A) -> UPair(A)
usame : (a : A) -> (b : B) -> upair a b == upair b a


Is this correct? If so, this can be easily emulated with Self-Types. Using Formality, which features Self-Types, we can write:

UPair : {A : Type} -> Type
\$self
{ ~P    : {wit : UPair(A)} -> Type
, upair : {a : A, b : A} -> P(upair(~A, a, b))
, usame : {a : A, b : A} -> upair(a, b) == upair(b, a)
} -> P(self)

upair : {~A : Type, a : A, b : A} -> UPair(A)
new(~UPair(A)){~P, upair, usame}
upair(a, b)


This behaves as the Reddit comment mentions. For example, it is impossible to write a first function, because the returned value can't differ for the [true, false], [false, true] cases, but it is possible to write a sum function for any commutative binary operator.

I've also attempted to implement a proof that UPair is isomorphic to Trit (which should hold since it has 3 elements, since [true, false] and [false, true] are the same). But I ran into some problems (== considers normal forms, so I guess I need extensional equality, and some way to prove those equalities are equivalent?).

In any case, my question is: did I "get it" and his proposed encoding indeed implements Quotient Types, or am I missing some piece?

For completeness, here is the full code with my experiments.

• You need to use usame : {~A : Type, a : A, b : A} -> upair(~A, a, b) == upair(~A, b, a) to prove upair(~Bool, true, false) == upair(~Bool, false, true). I don't know if you can define usame similarly to upair, but that's the job. – András Kovács Sep 10 '19 at 9:33
• What ar self types, and why do people implement type theory in Javascript? – Andrej Bauer Sep 10 '19 at 12:47
• @AndrejBauer I implement type theory in JavaScript because I think having type theory where normal people use computers (mobile, web-browsers) is more important than my own personal feelings about how bad JavaScript is. I can take this suffering for a greater good! – MaiaVictor Sep 10 '19 at 14:24
• @AndrásKovács I see. I don't think there is a way to make usame. Its presence as a "ghost constructor" of the Self Type affects pattern-matching exactly as expected, yet it can't be constructed as a "top-level" term, I think, so this isn't a proper implementation of higher inductive types... – MaiaVictor Sep 10 '19 at 14:31
• You could use a humane programming language and compile to JavaScript. I am amazed, though, that you can pull this off. I'll wait for an explanation of self-types to see if they have anything to do with higher inductive types. – Andrej Bauer Sep 10 '19 at 20:16