These are chat archives for typelevel/scala

27th
Mar 2017
Edmund Noble
@edmundnoble
Mar 27 2017 05:13
@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
Alexander Konovalov
@alexknvl
Mar 27 2017 05:19
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.
Edmund Noble
@edmundnoble
Mar 27 2017 05:19
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?
Alexander Konovalov
@alexknvl
Mar 27 2017 05:20
AFAIK it might cause some problems if someone pattern matches using its .type (?)
Edmund Noble
@edmundnoble
Mar 27 2017 05:21
Oh jeez I hope nobody matches on a Liskov's singleton type :'(
Alexander Konovalov
@alexknvl
Mar 27 2017 05:21
Universal equality yada yada :P I think the whole point of proving stuff is to erase it at the end :sparkles:
Edmund Noble
@edmundnoble
Mar 27 2017 05:21
Like yes you can write unsafeCoerce with it but that's the same as any singleton instance
Yeah, I agree :D
Alexander Konovalov
@alexknvl
Mar 27 2017 05:22
BTW I am thinking on a fully type-safe Matrix/Vector/Tensor library
using dependent types in Scala
Edmund Noble
@edmundnoble
Mar 27 2017 05:22
Ooooooh. Vector space monad?
Alexander Konovalov
@alexknvl
Mar 27 2017 05:22
scary quotes
"dependent types"
Edmund Noble
@edmundnoble
Mar 27 2017 05:22
"dependy types"
Alexander Konovalov
@alexknvl
Mar 27 2017 05:24
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
Edmund Noble
@edmundnoble
Mar 27 2017 05:24
Oh yeah, there is.
It's just you have to pass around your Value evidence everywhere and use its type member.
Alexander Konovalov
@alexknvl
Mar 27 2017 05:24
Yep
Edmund Noble
@edmundnoble
Mar 27 2017 05:24
It's just... impossible to prove you are using it correctly.
Alexander Konovalov
@alexknvl
Mar 27 2017 05:24
And you also need a comparison operator that lifts to type-level
Edmund Noble
@edmundnoble
Mar 27 2017 05:24
Yeah, exactly.
Alexander Konovalov
@alexknvl
Mar 27 2017 05:25
Value[N] == Value[M] ==> N === M
Edmund Noble
@edmundnoble
Mar 27 2017 05:25
Yeah, and we can't really do that. Can we?
Like without just church-encoding?
Alexander Konovalov
@alexknvl
Mar 27 2017 05:25
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
}
Edmund Noble
@edmundnoble
Mar 27 2017 05:26
Oof. What is this... Lifted ;)
Is there a <: Singleton bound somewhere in that Type member?
Alexander Konovalov
@alexknvl
Mar 27 2017 05:27
trait Lifted { self =>
  type Type >: self.type <: Lifted {
    type Type = self.Type
    type Value = self.Value
  }
  type Value
}
Edmund Noble
@edmundnoble
Mar 27 2017 05:27
...okay now I'm just confused
Alexander Konovalov
@alexknvl
Mar 27 2017 05:27
abstract class Nat protected () extends Lifted {
  type Value = Int
  type Type = Nat
}
final class Z extends Nat
final class S[N <: Nat] extends Nat
Edmund Noble
@edmundnoble
Mar 27 2017 05:27
Oh. Riiiiiight.
Alexander Konovalov
@alexknvl
Mar 27 2017 05:27
I want to pass Type and Value "implicitly"
so I do this weird trick
Edmund Noble
@edmundnoble
Mar 27 2017 05:28
as type members.
And how do you pass that?
You just pass the type param as Nat?
Alexander Konovalov
@alexknvl
Mar 27 2017 05:28
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
Edmund Noble
@edmundnoble
Mar 27 2017 05:29
Oh right. I see, that's what the bounds mean.
Alexander Konovalov
@alexknvl
Mar 27 2017 05:29
Because of that weird Type >: self.type constraint
Yeah
It doesn't work for everything, sometimes I am forced to pass Type explicitly
But for simple things it suffices
Edmund Noble
@edmundnoble
Mar 27 2017 05:30
Any nice examples I can show off? :D
Some preliminary results:
Edmund Noble
@edmundnoble
Mar 27 2017 05:33
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
Alexander Konovalov
@alexknvl
Mar 27 2017 05:33
(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
Edmund Noble
@edmundnoble
Mar 27 2017 05:35
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.
Alexander Konovalov
@alexknvl
Mar 27 2017 05:35
Reduce[S[S[Z]] + S[S[S[Z]]]] for instance returns S[S[Z]] + S[S[S[Z]]] === S[S[S[S[S[Z]]]]]
Edmund Noble
@edmundnoble
Mar 27 2017 05:36
Yes, quite nice. Almost like Idris ;)
Alexander Konovalov
@alexknvl
Mar 27 2017 05:36
So you can substititute anywhere
Edmund Noble
@edmundnoble
Mar 27 2017 05:36
Can you go backwards? That is, can you perform subtraction?
Alexander Konovalov
@alexknvl
Mar 27 2017 05:37
Not yet. Haven't thought about it.
And you can lift == to ===.
Edmund Noble
@edmundnoble
Mar 27 2017 05:37
Yeah, that's the killer feature.
That's what shapeless nat needs.
Alexander Konovalov
@alexknvl
Mar 27 2017 05:38
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:
Edmund Noble
@edmundnoble
Mar 27 2017 05:39
LOL
Mmmmm. Make a nice efficient product/coproduct encoding ;)
Alexander Konovalov
@alexknvl
Mar 27 2017 05:39
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
  }
}
Edmund Noble
@edmundnoble
Mar 27 2017 05:40
Ahead-of-time erasure! Proof elimination, from the source code ;)
Alexander Konovalov
@alexknvl
Mar 27 2017 05:40
This is a proof that Z commutes with respect to +.
The same one as you would write in Idris
Edmund Noble
@edmundnoble
Mar 27 2017 05:41
Yeah, you have some pre-order reasoning syntax going on there.
How long until the divergence checker kicks in ;)
Alexander Konovalov
@alexknvl
Mar 27 2017 05:42
Lol I don't think I will be proving stuff much, easier to just EqT.unsafeForce ;)
Edmund Noble
@edmundnoble
Mar 27 2017 05:42
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.
Alexander Konovalov
@alexknvl
Mar 27 2017 05:45
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.
Edmund Noble
@edmundnoble
Mar 27 2017 05:47
Is Exists not equivalent to Pi?
Wait, what are Pi and Sigma in Scala?
Alexander Konovalov
@alexknvl
Mar 27 2017 05:49
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]]]
Edmund Noble
@edmundnoble
Mar 27 2017 05:53
Aw shit. That looks nice.
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
Alexander Konovalov
@alexknvl
Mar 27 2017 05:57
Yeah, it's currently called catz (cats that are a bit too eXperimental for normal cats) :)
Edmund Noble
@edmundnoble
Mar 27 2017 05:58
I hope there's a bunch of kinds of functors :D
Is Int a kind?
Alexander Konovalov
@alexknvl
Mar 27 2017 05:59
so it's WIP atm
wdym? Int a kind?
Edmund Noble
@edmundnoble
Mar 27 2017 06:00
I mean do we have data kinds?
Alexander Konovalov
@alexknvl
Mar 27 2017 06:01
Mmm technically, aren't all data constructors types themselves in Scala?
So it's like DataKind
Edmund Noble
@edmundnoble
Mar 27 2017 06:01
Oh yes and singleton types, of course :D
Alexander Konovalov
@alexknvl
Mar 27 2017 06:03
Right now only base and category have any code
Pascal Voitot
@mandubian
Mar 27 2017 15:43
@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?
Alexander Konovalov
@alexknvl
Mar 27 2017 16:01
Nothing at the moment. I'll let you know if something comes up.
Pascal Voitot
@mandubian
Mar 27 2017 16:24
@alexknvl those Reduce.assert are quite astonishing... when you say you can erase if totality is proven, in scala, can you really erase?
Alexander Konovalov
@alexknvl
Mar 27 2017 16:55
Yes in Scalazzi world.
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 nulls)
Alexander Konovalov
@alexknvl
Mar 27 2017 17:01
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.
m4dc4p
@m4dc4p
Mar 27 2017 19:55
@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.
Paolo G. Giarrusso
@Blaisorblade
Mar 27 2017 20:35
@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)
Pascal Voitot
@mandubian
Mar 27 2017 21:14
@alexknvl Yep I see... that's quite logical and really cool actually
Edmund Noble
@edmundnoble
Mar 27 2017 21:47
@Blaisorblade I thought Pi was the pair :'(
Pi, product, of course! Only not ;)
Matthew Pocock
@drdozer
Mar 27 2017 22:09
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)
Matthew Pocock
@drdozer
Mar 27 2017 22:18
thanks @milessabin
Paolo G. Giarrusso
@Blaisorblade
Mar 27 2017 23:56
@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
This message was deleted
Edmund Noble
@edmundnoble
Mar 27 2017 23:58
Ah interesting.
Paolo G. Giarrusso
@Blaisorblade
Mar 27 2017 23:58
Naming things properly is a hard problem in computer science, while sometimes mathematicians have given up on it altogether ;-)