GADTs in scala confused.

24 views
Skip to first unread message

Chen Harry

unread,
Feb 27, 2018, 5:46:25 AM2/27/18
to scala...@googlegroups.com
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

unread,
Feb 27, 2018, 5:41:06 PM2/27/18
to Melbourne Scala User Group
Paul Chiusano's rundown of GADTs in Scala is useful:


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

unread,
Feb 27, 2018, 6:48:31 PM2/27/18
to scala...@googlegroups.com
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

unread,
Mar 8, 2018, 5:32:01 AM3/8/18
to scala...@googlegroups.com

Ben Hutchison

unread,
Mar 8, 2018, 6:41:37 AM3/8/18
to scala...@googlegroups.com
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

unread,
Mar 8, 2018, 5:42:36 PM3/8/18
to scala...@googlegroups.com
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

unread,
Mar 8, 2018, 10:39:17 PM3/8/18
to scala...@googlegroups.com
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 
Reply all
Reply to author
Forward
0 new messages