<p>I was trying to understand Quotient Types, and determine if Self-Types can be used to implement them. From a <a href="https://www.reddit.com/r/haskell/comments/54xdvz/quotient_types_for_programmers/" rel="nofollow noreferrer">Reddit post</a>,</p>
<blockquote>
<p>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:</p>
<pre><code>sumSet (Set s) = sum s
</code></pre>
<p>and we can write a function first:</p>
<pre><code>firstSet (Set s) = first s
</code></pre>
<p>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 [1].</p>
</blockquote>
<p>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 &quot;phantom constructor&quot; on your datatype, which returns an equality instead of a member of the datatype. As in,</p>
<pre><code>data UPair (A : Set) : Set where
  upair : (a : A) -&gt; (b : A) -&gt; UPair(A)
  usame : (a : A) -&gt; (b : B) -&gt; upair a b == upair b a
</code></pre>
<p>Is this correct? If so, this can be easily emulated with Self-Types. Using <a href="https://github.com/moonad/formality" rel="nofollow noreferrer">Formality</a>, which features Self-Types, we can write:</p>
<pre><code>UPair : {A : Type} -&gt; Type
  $self
  { ~P    : {wit : UPair(A)} -&gt; Type
  , upair : {a : A, b : A} -&gt; P(upair(~A, a, b))
  , usame : {a : A, b : A} -&gt; upair(a, b) == upair(b, a)
  } -&gt; P(self)

upair : {~A : Type, a : A, b : A} -&gt; UPair(A)
  new(~UPair(A)){~P, upair, usame}
  upair(a, b)
</code></pre>
<p>This behaves as the Reddit comment mentions. For example, it is impossible to write a <code>first</code> function, because the returned value can't differ for the <code>[true, false]</code>, <code>[false, true]</code> cases, but it is possible to write a <code>sum</code> function for any commutative binary operator.</p>
<p>I've also attempted to implement a proof that <code>UPair</code> is isomorphic to <code>Trit</code> (which should hold since it has 3 elements, since <code>[true, false]</code> and <code>[false, true]</code> are the same). But I ran into some problems (<code>==</code> considers normal forms, so I guess I need extensional equality, and some way to prove those equalities are equivalent?).</p>
<p>In any case, my question is: <strong>did I &quot;get it&quot; and his proposed encoding indeed implements Quotient Types, or am I missing some piece?</strong></p>
<p>For completeness, <a href="https://gist.github.com/MaiaVictor/62da9fb10f7a1222dc35930abb9ddee8" rel="nofollow noreferrer">here</a> is the full code with my experiments.</p>

CC BY-SA 4.0
2019-09-10T09:33:21.527Z
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
CC BY-SA 4.0
2019-09-10T12:47:08.140Z
What ar self types, and why do people implement type theory in Javascript?
Andrej Bauer
CC BY-SA 4.0
2019-09-10T14:01:47.700Z
It looks like higher inductive types to me.
Andrej Bauer
CC BY-SA 4.0
2019-09-10T14:24:12.047Z
@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
CC BY-SA 4.0
2019-09-10T14:25:51.097Z
@AndrejBauer we will add a Self-Types explanation on [Formality's documentation](https://docs.formality-lang.org) soon. There is [Aaron's paper](https://homepage.divms.uiowa.edu/~astump/papers/fu-stump-rta-tlca-14.pdf), but it is slightly outdated at this point...
MaiaVictor
CC BY-SA 4.0
2019-09-10T14:26:30.440Z
@AndrejBauer that'd be good! Why you think so, though?
MaiaVictor
CC BY-SA 4.0
2019-09-10T14:31:32.780Z
@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
CC BY-SA 4.0
2019-09-10T20:16:00.317Z
You could use a [humane programming language](http://www.ocaml.org/) 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
CC BY-SA 4.0
2019-09-10T21:04:32.037Z
@AndrejBauer I've considered Haskell, but its JS backend is awfulI, so I've started the project on Rust, but its closure implementation was terribly slow, making HOAS impossible. OCaml would be good perhaps, but having to deal with FFI and compilation stuff could slow down my progress. JS is not that bad if you do it defensively. You can almost write pseudo-Haskell on it, and people surely underestimate the fact JS has, hands down, the most mature runtimes in the world! (:
MaiaVictor
CC BY-SA 4.0
2019-09-10T21:07:22.590Z
Why would you have to deal with FFI? You need a modicum of it to interact with JS, and of course you wouldn't implement the UI in OCaml, that would be crazy. But I agree, the JS runtimes are insane.
Andrej Bauer
CC BY-SA 4.0
2019-09-10T21:10:57.900Z
@AndrejBauer not sure how mature OCaml->JS is, but see http://provit.fm, for example, a website we're developing where you can post "type bounties" for people to prove. Including Formality on it was as easy as `require("formality")`. An OCaml implementation would need to generate a proper CommonJS module with everything working, including XHR requests, filesystem management, detecting whether you're on a website context or in a terminal... there are some nasty, nasty stuff required to make JS work in places. I doubt the compiler would nail it and not give me any headache at all. Or would it?
MaiaVictor
CC BY-SA 4.0
2019-09-10T21:11:42.487Z
@AndrejBauer Self-Types are surprisingly easy to understand... they just allow a type to access its value. So, if `foo : self x. P(x)`, then `self-elim foo : P(foo)`. And that's it, I guess! The fun part is what can be done with that. I'll notify you when I write a dedicated article!
MaiaVictor
CC BY-SA 4.0
2019-09-11T05:00:12.933Z
@AndrejBauer For definition and properties of Self Types please take a look at [Section 5.2](https://fermat.github.io/document/papers/dissertation.pdf) of Peng Fu thesis or at the paper [Self Types for Dependently Typed Lambda
Encodings](https://fermat.github.io/document/papers/rta-tlca.pdf). Among other things they allow you to prove induction without inductive types.  

I for one am amazed why such an elegant and powerful construct isn't more well known.
Łukasz Lew
CC BY-SA 4.0
2019-09-12T13:14:59.657Z
In order to check that your definition of quotients is correct, I think you would want to prove two things. The first is the universal property of a quotient, that $$ A / R \to B \cong \{f : A \to B \mid \forall a, a' \in R.\ f(a) = f(a')\}$$. The second, which is often more difficult to achieve but very important, is effectivity. Effectivity essentially says that if $q(a) = q(a') : A / R$, then $R(a, a')$. Both of these are provable with the hProp HIT quotient, but the latter is a well-known thorn in the side of type-theoretic quotients. Here = is internal/typal equality. Not definitional.
daniel gratzer
<type-theory>
Is my understanding regarding how to implement Quotient Types correct?
MaiaVictor
# Is my understanding regarding how to implement Quotient Types correct?

(Asked by: username_0 on 2019-09-09)

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 [1].

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.

**Tags:** type-theory

> **Comments:**
> **username_1**: 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.  
> **username_2**: What ar self types, and why do people implement type theory in Javascript?  
> **username_2**: It looks like higher inductive types to me.  
> **username_0**: @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!  
> **username_0**: @AndrejBauer we will add a Self-Types explanation on [Formality's documentation](https://docs.formality-lang.org) soon. There is [Aaron's paper](https://homepage.divms.uiowa.edu/~astump/papers/fu-stump-rta-tlca-14.pdf), but it is slightly outdated at this point...  
> **username_0**: @AndrejBauer that'd be good! Why you think so, though?  
> **username_0**: @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...  
> **username_2**: You could use a [humane programming language](http://www.ocaml.org/) 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.  
> **username_0**: @AndrejBauer I've considered Haskell, but its JS backend is awfulI, so I've started the project on Rust, but its closure implementation was terribly slow, making HOAS impossible. OCaml would be good perhaps, but having to deal with FFI and compilation stuff could slow down my progress. JS is not that bad if you do it defensively. You can almost write pseudo-Haskell on it, and people surely underestimate the fact JS has, hands down, the most mature runtimes in the world! (:  
> **username_2**: Why would you have to deal with FFI? You need a modicum of it to interact with JS, and of course you wouldn't implement the UI in OCaml, that would be crazy. But I agree, the JS runtimes are insane.  
> **username_0**: @AndrejBauer not sure how mature OCaml->JS is, but see http://provit.fm, for example, a website we're developing where you can post "type bounties" for people to prove. Including Formality on it was as easy as `require("formality")`. An OCaml implementation would need to generate a proper CommonJS module with everything working, including XHR requests, filesystem management, detecting whether you're on a website context or in a terminal... there are some nasty, nasty stuff required to make JS work in places. I doubt the compiler would nail it and not give me any headache at all. Or would it?  
> **username_0**: @AndrejBauer Self-Types are surprisingly easy to understand... they just allow a type to access its value. So, if `foo : self x. P(x)`, then `self-elim foo : P(foo)`. And that's it, I guess! The fun part is what can be done with that. I'll notify you when I write a dedicated article!  
> **username_3**: @AndrejBauer For definition and properties of Self Types please take a look at [Section 5.2](https://fermat.github.io/document/papers/dissertation.pdf) of Peng Fu thesis or at the paper [Self Types for Dependently Typed Lambda Encodings](https://fermat.github.io/document/papers/rta-tlca.pdf). Among other things they allow you to prove induction without inductive types.    I for one am amazed why such an elegant and powerful construct isn't more well known.  
> **username_4**: In order to check that your definition of quotients is correct, I think you would want to prove two things. The first is the universal property of a quotient, that $$ A / R \to B \cong \{f : A \to B \mid \forall a, a' \in R.\ f(a) = f(a')\}$$. The second, which is often more difficult to achieve but very important, is effectivity. Effectivity essentially says that if $q(a) = q(a') : A / R$, then $R(a, a')$. Both of these are provable with the hProp HIT quotient, but the latter is a well-known thorn in the side of type-theoretic quotients. Here = is internal/typal equality. Not definitional.  

---

## 0 answers

