GADTs in scala confused.

[Chen Harry]

I have following code:

  sealed trait F[A]

  final case class FInt(a: Int) extends F[Boolean]

  final case class FF[A](a: A) extends F[Either[Throwable, A]]

  final case class FOption[A](o: Option[A]) extends F[Either[Throwable, A]]

  def f[A](a: F[A]): A = a match {

    case FInt(a)    => a > 10

    case FF(a)      => Right(a).map(_ => "yyy") // why accept this?

    case FOption(o) => o.fold[Either[Throwable, A]](Left(new Exception("")))(x => Right(x)) //why reject this?

  }

I expect the compiler reject the "FF(a)" case but it accepted it.

I want the compiler accept the "FOption(o)" case but rejected by the compiler. :)

ideas? or I did something wrong?

Cheers,

Harry

[Lachlan O'Dea]

Paul Chiusano's rundown of GADTs in Scala is useful:

https://gist.github.com/pchiusano/1369239

I don't understand why it's necessary, but pattern matching using existential types seems to do what you want:

sealed trait F[A]

  final case class FInt(a: Int) extends F[Boolean]

  

  final case class FF[A](a: A) extends F[Either[Throwable, A]]

  final case class FOption[A](o: Option[A]) extends F[Either[Throwable, A]]

  def f[A](a: F[A]): A = a match {

    case FInt(a) => a > 10

    case ff: FF[a] => Right(ff.a).map(_ => "yyy") // now rejected - found : String("yyy") required: a

    case fo: FOption[a] => fo.o.fold[Either[Throwable, a]](Left(new Exception("")))((x: a) => Right(x)) // now accepted

  }

Lachlan.

[Chen Harry]

Thank you very much, Lachlan. That's is exactly what I want.. seems that constructor pattern match lost the type information. I am curious how Scalac unify the existential type 'a' and 'A' -- how to prove that 'a' =:= 'A' ? 

Thanks again, that is really helpful.

Cheers,

Harry 

--
You received this message because you are subscribed to the Google Groups "Melbourne Scala User Group" group.
To unsubscribe from this group and stop receiving emails from it, send an email to scala-melb+...@googlegroups.com.
To post to this group, send email to scala...@googlegroups.com.
Visit this group at https://groups.google.com/group/scala-melb.
For more options, visit https://groups.google.com/d/optout.

[Chen Harry]

Support for GADTs in Dotty http://dotty.epfl.ch/blog/2018/03/05/seventh-dotty-milestone-release.html

[Ben Hutchison]

Interesting. Haven't been following Dotty closely but the erased modifier mentioned in the release notes looked appealing. 

I've been studying Idris recently and it's compile time proofs rely heavily on passing around implicit params that certify some desired property. eg that two lists are the same length. The erased modifier let's you use that technique with  confidence there won't be runtime overheads introduced. 

Ben

To unsubscribe from this group and stop receiving emails from it, send an email to scala-melb+unsubscribe@googlegroups.com.

To post to this group, send email to scala...@googlegroups.com.
Visit this group at https://groups.google.com/group/scala-melb.
For more options, visit https://groups.google.com/d/optout.

--

You received this message because you are subscribed to the Google Groups "Melbourne Scala User Group" group.

To unsubscribe from this group and stop receiving emails from it, send an email to scala-melb+unsubscribe@googlegroups.com.

[Chen Harry]

Idris is interesting. might I ask whether it is Turing complete?

To unsubscribe from this group and stop receiving emails from it, send an email to scala-melb+...@googlegroups.com.

To post to this group, send email to scala...@googlegroups.com.
Visit this group at https://groups.google.com/group/scala-melb.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "Melbourne Scala User Group" group.

To unsubscribe from this group and stop receiving emails from it, send an email to scala-melb+...@googlegroups.com.

To post to this group, send email to scala...@googlegroups.com.
Visit this group at https://groups.google.com/group/scala-melb.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "Melbourne Scala User Group" group.

To unsubscribe from this group and stop receiving emails from it, send an email to scala-melb+...@googlegroups.com.

[Ben Hutchison]

Oh yeah, it’s intended as a “practical” language for applied use. Although far off Scala or Haskell in maturity. 

It’s got a totality checker but it’s opt-in, ie off by default