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 :see__no__evil: 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".