Typeclasses, Propositions, Data types

Extra attributes on post: XmlAttr(name=original_url, value=String(value=https://gitter.im/scalaz/scalaz?at=5abade97bb1018b37a3117af))

A: I just had an Eureka moment when I realized that recursors for higher-inductive types like Set[A] actually guarantee that no one will be able to observe the order.

trait SetSig {
    type F[A]
    def empty[A]: F[A]
    def singleton[A](a: A): F[A]
    def union[A : C](a: F[A], b: F[A])(...): F[A]

    // Use your imagination from this point on
    def assoc[A : C](a: F[A], b: F[A], c: F[A]): union(union(a, b), c) =
      union(a, union(b, c))
    def commute[A : C](a: F[A], b: F[A]): union(a, b) =
      union(b, a)
    // ...
}

object RBTree extends SetSig {
    // concrete implementation of an abstract type
    // has to implement laws as well
}
type RBTree[A] = RBTree.F[A]

// Recursor
def rec[A, Z](fa: RBTree[A])(
    empty: Z,
    singleton: A => Z,
    union: C[A] => (Z, Z) => Z,
    assoc: C[A] => (a: Z, b: Z, c: Z) =>
      union(union(a, b), c) = union(a, union(b, c))
    // ...
): Z

H: "Har har" at that comment. So you have to produce both values of type Z and proofs about those values (to the extent there's a difference).

A: It's a weakened form of induction. You can make it accept Z[_] and return Z[A] and then on top of that add dependent types to get proper induction.

H: Wouldn't the induction principle be more general than that though?

A: Here, I'll write it out... I think it would look something like this:

def ind[A, Z[fa : F[A]]](a: F[A])(
    empty': Z[empty[A]],
    singleton': (a: A) => Z[singleton(a)],
    union': C[A] => (a: F[A], b: F[A]) => (Z[a], Z[b]) => Z[union(a, b)],
    assoc': C[A] => (a: F[A], b: F[A], c: F[A]) => (a': Z[a], b': Z[b], c': Z[c]) => union'(union'(a', b'), c') = union'(a', union'(b', c'))
    // ...
): C[a]

H: I'm still not sure how I feel about the ordering of an ISet / ==>> being observable. If you swap Order for Hash I can give you an otherwise-functionally-identical data structure. Maybe we need:

class SetLike f where
    type SetR :: Constraint

    empty :: f a
    single :: SetR a => a -> f a
    union :: SetR a => f a -> f a -> f a
    elem :: SetR a => f a -> a -> Bool
    setMap :: SetR b => (a -> b) -> f a -> f b

>

E: That is not observable ordering. It's "give me the nth element". Those are very different.

H: How so? I mean that I can observe that the elements of my set (map) are ordered somehow. Obviously I can't go get the ordering itself.

E: No, you can't, you aren't observing any internal structure. You're asking "give me the nth element according to my Ord a". The internal structure has nothing to do with that. In this case, they coincide in a nice way, and that makes this operation faster.

H: Except you don't provide an Ord a.

E: "A ==>> B has an elemAt(i: Int) method which picks the ith least pair according to A's ordering".

H: Mmhm.

E: So A has an ordering. No?

H: Well yes, you had to give it to make the set and we're going to :seenoevil: and imagine typeclass coherence so it's the one ordering for A. Okay, so I think I get what you're saying: because we have an Ord a by construction, looking up by index is using that fact, not anything internal. That makes sense.

A: If you use identity for Eq[A], there is at most one instance. In some sense there is also at most one HashEq[A] <: Eq[A], but I am not sure what "sense" it is. So typeclass coherence follows from the laws. Same as Functor[F] AFAIU. There is at most one lawful instance, hence DeriveFunctor extension in Haskell.

A: Now I want Idris with higher-inductive (quotient?) types sob. H, what if reference equality could return a type such that you had to prove that you don't use it for evil (that you don't violate parametricity "in the end")...

H: How do you mean?

A: Well, think how higher inductive types can prevent you from observing the internal implementation of a set.

H: Right.

A: Perhaps there is a way to make it so that the result type of a reference comparison could not be used to violate parametricity. You would have to prove that no one else can observe that you have violated it. So eq : [A] (a : A, b : A) : RefEq[A, a, b] such that RefEq[A, a, b] has an induction principle that doesn't allow you to write non-parametric code.

H: I am trying to come up with such an induction principle. The awkward bit is (on the JVM) reference equality can be applied to any kind of object.

A: Say you made a Set like above, but removed the constraint C. I can implement an semi-efficient version of it using eq and hashCode. And you wouldn't be able to observe this abuse of reference equality.

H: Hmm. Well, assuming you used identityHashCode.

A: Yeah.

H: So Eq[Ord[A]] makes no sense in Haskell but "works" in scala because we don't distinguish constraints and types.

A: Eq[Ord[A]] makes a lot of sense to me, it always returns true trollface. I think Haskell's treatment of constraint kind is wrong.

H: How so?

A: They have too much custom syntax. Typeclasses are just propositions but we guarantee that they are IsProp[_] by convention. Is Is[A, B] a typeclass? There is at most one instance.

E: That's not all of what makes a type class

A: In Haskell you have to define one Is as a data type and one as a typeclass (~). And it is meaningless duplication.

E: There's a reason to define Is as a data type? Why?

H: Is being type equality?

data Is a b where
  refl :: Is a a

Or a different one?

A: This one will work.

E: All pattern matching on Is does is introduce an a ~ b.

A: More generally data Is (a :: k) (b :: k) = MkIs (forall (f :: k -> *) . f a -> f b). Yes, so there are two different concepts. Why?

E: What is the difference in Haskell? Between those two things? Practically?

A: They are the same thing.

E: Okay, then why do I have to define any of them when they're all equivalent to ~?

A: Say you didn't have GADTs...

E: Why? I do have GADTs, I have them all over the place.

H: Isn't the whole point so you can do

safeCoerce :: Is a b -> a -> b
safeCoerce refl a = a

or whatever?

A: You have tons of features which duplicate functionality.

E: Why can't you be happy with (a ~ b) => a -> b. You can build HoTT out of that functionality

E: If you need to pass it as a value, why not Dict (a ~ b)? If you don't, what's the problem?

A:

• Typeclasses : at most one instance (by convention), have nice inference.
• Propositions : at most one instance (by definition), little to no inference (have to prove things manually).
• Data types : more than one instance, no inference (and thank god).

I want to be able to manipulate some typeclasses manually, because they are actually propositions as in Eq[A].contramap or Functor[F].isoMapK.

E: It's not a proposition anymore once you contramap it, no? Are you saying that during instance construction, you want to be able to say "this instance is just that instance, with a contramap thrown across"?

A: Both Eq[A] and Functor[F] are propositions. Of course when you map, you would have to map laws as well.

E: ?

H: I do really like Contravariant[Eq] even though it's probably sinful. As a convenience if not a principle.

E: I get the idea of being able to treat instances as values, only while defining other instances. To me that's appealing. I see the lessening of boilerplate, I see the way this helps avoid forgetting to overload defaults.

A: Yeah, that would be great as well. H, it's not always sinful, that's the point. It is not sinful when F is both a typeclass and a proposition, you can not produce anything but the correct instance.

H: Right. Are there non-proposition typeclasses?

A: Sure, most are not really propositions, they are propositions by convention only.

E: Let's not go into "type classes are really not propositions, we're just pretending".

A: But we are.

E: That line of thinking does not help build sane programs. It helps undermine what type classes mean. See "type classes vs the world".

A: I have, and I agree with everything Ed says there but...

Unknown tag: q

A: This is an orthogonal issue entirely.

Unknown tag: q

A: I am not disputing the value of having a convention.

E: But I fail to see how it's orthogonal.

A: You can do all sorts of things to propositions, like map, zip, etc. You should be able to do that to typeclasses with the same syntax as usual.

E: Things that don't violate coherence?

A: As long as there are guarantees you don't break coherence.

E: map does violate coherence, zip doesn't.

A: That's not always the case.

E: When there's only one morphism to the type in question?

A:

class Uninhabited a where
  void :: a -> Void

I am free to contramap it with any total function. contramap f (p :: Uninhabited a) :: Uninhabited b is identical to any other Uninhabited b.

E: Riiiiight.

A:

class Inhabited a where
    proof :: (a -> Void) -> Void

this one can be mapped by any total function.

E: Can you give an example not involving Void? It seems like it's impossible to reason in general without dependent types whether an operation will take propositions to propositions.

A:

class (~) a b where
    proof :: forall f . f a -> f b

can be flip'ped, andThen'd, etc

E: Sure, but how do you know? Also, I'm not sure this is useful. Doesn't the solver know from a ~ b and b ~ c that a ~ c, or is that impossible?

A: In Haskell it does, but there are no such rules for Inhabited a. There are more complex propositions.

E: Let's take it back to say, Eq. What do you do about Eq? What is a safe transformation?

A:

class Eq t where
  (==) :: (a :: t) -> (b :: t) -> Dec (a = b)
  -- plus laws?

is a proposition.

E: Dependent types, then?

A: And I think all laws follow from the definition (reflexivity, transitivity, commutativity, substitutability), although I am not entirely sure.

E: I think judgmental equality needs some form of dependent types, no?

A: Yeah, I doubt you can implement it in Haskell yet. There are other examples, if you have a bracket type, which is like existence without observable value. I think it can be replaced with Inhabited a in most cases.

E: I should hope I do, I love squash. I think that's what it is, yeah. Dict (Inhabited a) should be equivalent.

A: Then type Finite s = Inhabited (exists n :: Nat . Iso (Fin n ) s) is a proposition.

E: Mhmhmhm, gotcha.

A: It can be mapped as well.

E: Mapped how?

A: contra, wait no, iso.

E: Right that I get, for sure.

A: According to Schröder–Bernstein theorem, a pair of injective functions should be enough.

E: Mmmm, yes. Oh wait,

Unknown tag: q

Rejected. LEM is verboten.

A: Not for finite sets. And LEM can be added for some propositions.

E: Wait, we're not talking about those. The type s is not a proposition.

A: Functor[F] is a proposition, but I wouldn't want a LEM for it. That's definitely non-constructive. In Scala there is an assortment of propositional types related to subtyping: `<~<, Covariant, Injective (also in Haskell), </<`, etc. And I think squashing types gives you propositions with the same API except every result has to squashed as well.

E: But do they have computational content? Like, what happens when you map with an [(A => B)]?

A: You map [F[A]] with A => B (with [A => B]) and get [F[B]].

E: But there is no computation going on.

A: Well, that's squashing. It's different for Eq or Functor or even Finite.

E: Aren't those all props?

A: Yes, but they have "computational meaning".

E: Hmm.

A: Hence you don't really want LEM for them.

E: Right you don't want LEM.

A: But "LEM" can be added like so

lem :: [Either a (a -> Void)]

And for some types you can do

lem :: [a] -> a

The reason I am calling this lem is because

Inhabited a -> a
  = ((a -> Void) -> Void) -> a
  = Not (Not a) -> a

It is double negation.

E: I think that makes sense as a formulation of lem. Regardless, Eq[A] => Eq[B] while preserving that Eq[B] is a prop requires that B => A is a prop.

A: No. There is a A => [A] for any A.

E: That's not what I mean. I mean that B => A has to be isomorphic to Unit. Only if Eq[A] and B => A are isomorphic to Unit, can (Eq[A], B => A) => Eq[B] be an isomorphism. That's essentially what you're providing.

A: You can contramap with any injective function.

E: You need to prove that all of your operations over type classes are isomorphisms. Because that's how you know everything is isomorphic to unit.

A: No, any injection will work. Eq[A] tells you that there is no way to distinguish between values if it returns true, so Eq[A] must compare "every bit" of A. Therefore an injection of B into A composed with such comparison will compare "every bit" of B.

E: Right, which means the B => A must use "every bit" of B to produce "every bit" of A.

A: No

E: Otherwise you could use "every bit" of B to produce the bits of A in different ways.

A: Sure, but that's not observable.

E: Hm, right, as long as it's injective and doesn't throw away any of the bits. Gotcha, makes sense. So this doesn't make sense for any equivalences?

A: Doesn't because they don't have to compare "all bits" and in general are non-unique.

E: But it does make sense for Functor, because there can only be one lawful instance?

A: Yes, any transformation that preserves the laws will give you the same instance. I think that Hashable can also be made into a proposition, but you would need to very carefully prevent the person using it from observing any specifics about your hashing algorithm. It's rarely the case that I want to know whether hash(x) is divisible by 11 smile.

A: E, Liquid Haskell could provide a way to get refinements as values, e.g. p :: x > 0 = True, since identity is a prop with [a] -> a (thank god for UIP).

A: H, for reference equality induction ((a eq b).ind(f: true => Z, g: false => Z) : Z) you need to supply a proof that the result : Z does not depend on whether it gives you true or false under the assumption that a = b and it should still be possible to use the result with quotient types (you know what the value of reference equality is, but for anyone else it's unobservable). You can even throw in universal equality and ensure that everyone uses it only for optimization.

A:

// assuming dependent types
def eq(a : A, b : A): RefEq[A, a, b]
sealed trait RefEq[A, a, b] {
    // higher-inductive pattern match
    def cata[Z](true: (a = b) => Z, false: => Z)(p: (q : a = b) => true(q) = false): Z
}

if a and b are identical, both cases should return the same result and you get a proof of identity from reference equality in the true case.

A: Behold, "Universal Referentially Transparent Reference Equality".