4
$\begingroup$

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.

$\endgroup$
14
  • 1
    $\begingroup$ 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. $\endgroup$ – András Kovács Sep 10 '19 at 9:33
  • 1
    $\begingroup$ What ar self types, and why do people implement type theory in Javascript? $\endgroup$ – Andrej Bauer Sep 10 '19 at 12:47
  • 1
    $\begingroup$ @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! $\endgroup$ – MaiaVictor Sep 10 '19 at 14:24
  • 1
    $\begingroup$ @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... $\endgroup$ – MaiaVictor Sep 10 '19 at 14:31
  • 1
    $\begingroup$ 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. $\endgroup$ – Andrej Bauer Sep 10 '19 at 20:16

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.