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$ Sep 10, 2019 at 9:33
  • 1
    $\begingroup$ What ar self types, and why do people implement type theory in Javascript? $\endgroup$ Sep 10, 2019 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, 2019 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, 2019 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$ Sep 10, 2019 at 20:16

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.