@alexknvl But you have to! Or at least, that's what Stephen says ;)

Or at least, he seems to imply that it's one of the strongest benefits of Liskov.

Allocation is *such* a bummer though

No, you really don't and you shouldn't. It's a type with a single possible value.

@edmundnoble So you can erase it entirely.

Yes, Stephen's point is that you shouldn't erase it entirely.

Because it does actually make for convincing evidence of soundness; the fact that it's there is... comforting?

AFAIK it might cause some problems if someone pattern matches using its

`.type`

(?)
Oh jeez I hope nobody matches on a Liskov's singleton type :'(

Universal equality yada yada :P I think the whole point of proving stuff is to erase it at the end :sparkles:

Like yes you can write unsafeCoerce with it but that's the same as any singleton instance

Yeah, I agree :D

BTW I am thinking on a fully type-safe Matrix/Vector/Tensor library

using dependent types in Scala

"dependent types"

I had this eureka moment recently, when I realized that there is this misconception that you can't use

`Vec[N <: Nat, A]`

in Scala for values that depend on runtime
And it's entirely false

It's just you have to pass around your

`Value`

evidence everywhere and use its type member.
It's just... impossible to prove you are using it correctly.

And you also need a comparison operator that lifts to type-level

Like without just church-encoding?

```
final case class Value[N <: Lifted](value: N#Value) extends AnyVal { n =>
def ==[M <: N#Type](m: Value[M])(implicit eq: Equiv[N#Value]): Option[EqT[N#Type, N, M]] =
if (eq.equiv(n.value, m.value)) Some(BoundedLeibniz.unsafeForce[Nothing, N#Type, N, M])
else None
}
```

Is there a

`<: Singleton`

bound somewhere in that `Type`

member?
```
trait Lifted { self =>
type Type >: self.type <: Lifted {
type Type = self.Type
type Value = self.Value
}
type Value
}
```

```
abstract class Nat protected () extends Lifted {
type Value = Int
type Type = Nat
}
final class Z extends Nat
final class S[N <: Nat] extends Nat
```

so I do this weird trick

And how do you pass that?

You just pass the type param as

`Nat`

?
Yeah, so that they don't appear in type signatures all over the place.

No, given

`S[Z]`

for instance you can do
`S[Z]#Type`

and get `Nat`

`S[Z]#Value`

and get `Int`

.
And it's encoded in such a way that if

`A <: Lifted`

, then `A <: A#Type`

Yeah

It doesn't work for everything, sometimes I am forced to pass

`Type`

explicitly
But for simple things it suffices

Some preliminary results:

I did something similar but ultimately removed it; I have a DSL with

`case class Definition(numParams: Int, body: List[A] => P)`

and I used `Sized`

but my use-site was right next to it anyway, so I took it out; and shapeless Nat doesn't allow you to do it nicely
`(1 :: 2 :: 3 :: Nil).map(_ + 2) ++ (1 :: 2 :: Nil)`

works, `(a: Vec[N, A]) ++ (b: Vec[M, A]): Vec[N + M, A]`

If

`N`

or `M`

are known, then `simplify`

adds `N + M`

or simplifies it to `S[...[M]...]`

(if `M`

is unknown).
`Reduce[N + M]`

reduces the type as much as possible
`Value[N + M]`

computes the value if there is a `Value[N]`

and `Value[M]`

in scope
I see. I believe this is what the difference is between Scala and a real dependently typed language; user-defined beta-reduction instead of the language's beta reduction.

`Reduce[S[S[Z]] + S[S[S[Z]]]]`

for instance returns `S[S[Z]] + S[S[S[Z]]] === S[S[S[S[S[Z]]]]]`

Can you go backwards? That is, can you perform subtraction?

And you can lift

`==`

to `===`

.
That's what shapeless nat needs.

That's really all you need for

`Vec[N, A]`

to work at runtime. I am currently investigating `Fin`

, `<`

, and `Product`

/`Coproduct`

.
```
object Proofs {
implicit def plusIsAssociative[A <: Nat, B <: Nat, C <: Nat]: EqT[Nat, A + (B + C), (A + B) + C] =
EqT.unsafeForce[Nothing, Nat, A + (B + C), (A + B) + C]
implicit def plusIsCommutative[A <: Nat, B <: Nat]: EqT[Nat, A + B, B + A] =
EqT.unsafeForce[Nothing, Nat, A + B, B + A]
}
```

:sparkles:

Mmmmm. Make a nice efficient product/coproduct encoding ;)

I can prove them as well, but it doesn't make sense since the reason it works so well in Idris is that it can erase proofs

So here I just erased them ahead of time :P

```
final case class PlusCommutes[m <: Nat](proof: m === (m + Z))
object PlusCommutes {
implicit def plus_commutes_Z_1: PlusCommutes[Z] =
PlusCommutes(Reduce[Z + Z].flip)
implicit def plus_commutes_Z_2[n <: Nat](rec: PlusCommutes[n]): PlusCommutes[S[n]] = PlusCommutes {
val p1: (S[n] + Z) === S[n + Z] = Reduce[S[n] + Z]
val p2: n === (n + Z) = rec.proof
val p3: S[n] === S[n + Z] = p2.lift[Nat, S]
(p1 andThen p3.flip).flip
}
}
```

Ahead-of-time erasure! Proof elimination, from the source code ;)

The same one as you would write in Idris

Yeah, you have some pre-order reasoning syntax going on there.

How long until the divergence checker kicks in ;)

Lol I don't think I will be proving stuff much, easier to just

`EqT.unsafeForce`

;)
Hehehe I would probably do the same. Still, very nice to have a set of facts to work with instead of forcing casts to the use site.

```
def listToVec[A](s: List[A]): Exists[Nat, ({type L[N <: Nat] = (Value[N], Vec[N, A])})#L] = {
type L[N <: Nat] = (Value[N], Vec[N, A])
s match {
case Nil =>
new Exists[Nat, L] {
type Type = Z
def value: (Value[Z], Vec[Z, A]) = (implicitly, Vec.Nil)
}
case x :: xs =>
val rec: Exists[Nat, L] = listToVec(xs)
new Exists[Nat, L] {
type Type = S[rec.Type]
def value: (Value[Type], Vec[Type, A]) =
(Nat.s(rec.value._1), x :: rec.value._2)
}
}
}
```

This is pretty ugly and still needs cleanup. AFAIU

`Exists`

can be replaced with `Pi`

or `Sigma`

.
Wait, what are

`Pi`

and `Sigma`

in Scala?
Yeah, I think

`Pi`

is `Exists`

as in above. A pair of `a: A`

and `b: B a`

.
But I think that having a custom constructor might look better, e.g.

```
trait Pi[T <: Lifted, F[_ <: T#Type]] {
type N <: T#Type
def first: Value[N]
def second: F[N]
}
```

`Pi[Nat, Lambda[N <: Nat => Vec[N, A]]]`

`Nat Pi Lambda[N <: Nat => Vec[N, A]]`

Are you releasing something with all of these kind polymorphic dependently-typed tools eventually?

I think it's something to at least consider for the future of cats

Yeah, it's currently called

`catz`

(cats that are a bit too eXperimental for normal cats) :)
Is

`Int`

a kind?
No functors yet. I don't like this design - https://github.com/alexknvl/subcats/blob/master/core/src/main/scala/subcats/functor/Functor.scala

so it's WIP atm

wdym?

`Int`

a kind?
Mmm technically, aren't all data constructors types themselves in Scala?

So it's like

`DataKind`

Right now only

`base`

and `category`

have any code
@alexknvl you're melting my brain with all those stuff ;) marvellous that it compiles in scala actually whatever one can say about this compiler :)

What is currently failing in kind-polymorphism in case I must improve something blocking?

Nothing at the moment. I'll let you know if something comes up.

@alexknvl those Reduce.assert are quite astonishing... when you say you can erase if totality is proven, in scala, can you really erase?

You can observe such things in Scala because of

`eq`

, `hashCode`

etc.
If you know that a function is pure & total and it returns a singleton, there is no need to evaluate it.

Just like there is no need to evaluate a pure & total

`A => Unit`

(ignoring `null`

s)
Similarly, if someone gives you a pure & total

`A => Nothing`

, there should be no way for you to run it, since `A`

is guaranteed to be empty.
@SethTisue I managed to fix that bug (https://issues.scala-lang.org/browse/SI-7809) on the flight home. Here's my PR - scala/scala#5807. I signed the CLA first thing. Let me know what else I can do to get the fix looked at! Really appreciate your help, I woudlnt' have managed it otherwise.

@alexknvl I now saw your "Pi" type, but that's really "Sigma" instead

and yes, their names are enormously confusing

but Pi(x: T1)T2 is just the dependent function space (x: T1) -> T2

(also called by some dependent product, because the graph of such a function is the product of a copy of T2 for each possible value for x: T1)

while Sigma(x: T1) T2 is the dependent pair (x: T1, y: T2) (where x can appear in T2), also called either dependent product (because it's a pair) or dependent sum (because it's a sum of a copy of T2 for each possible value in T1)

@alexknvl Yep I see... that's quite logical and really cool actually

Pi, product, of course! Only not ;)

So can we do this in scala using macros magic? Or are our macros not powerful enoug? https://www.youtube.com/watch?v=qlKZKN7il7c

(type providers)

@edmundnoble well, as I mentioned, Pi *is* a dependent product, only the other kind — "dependent product" can mean "Sigma" or "Pi" depending on authors

the best solution I had heard is to stick to Sigma and Pi types, since they only have one correct meaning

but that doesn't help if you've been confused by the terminology

Naming things properly is a hard problem in computer science, while sometimes mathematicians have given up on it altogether ;-)