Last active
June 24, 2016 07:00
-
-
Save AndreasKostler/d6f0734dccbd598c8c1bc79a2b42d0dc to your computer and use it in GitHub Desktop.
Unboxed recursive union types via the Curry Howard Correspondence
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| object UnionTypes { | |
| private type ¬[A] = A => Nothing | |
| private type ¬¬[A] = ¬[¬[A]] | |
| private type ∈[S, T <: Disjunction] = ¬¬[S] <:< ¬[T#D] | |
| private type ∉[S, T <: Disjunction] = ¬¬[S] <:!< ¬[T#D] | |
| /** `S` is `T`. */ | |
| type Is[S, T] = ∈[S, OneOf[T]#Or[Nothing]] | |
| /** `S` must be in `T`. */ | |
| type In[S, T <: Disjunction] = ∈[S, T] | |
| /** `S` must not be in `T`. */ | |
| type NotIn[S, T <: Disjunction] = ∉[S, T] | |
| /** `T`. */ | |
| type OneOf[T] = { type Or[S] = (Disjunction {type D = ¬[T]})#Or[S] } | |
| /** Defines alternative vaues for `T`. */ | |
| trait Disjunction { | |
| self => | |
| type D | |
| type Or[S] = Disjunction { | |
| type D = self.D with ¬[S] | |
| } | |
| } | |
| type TP[T] = T In OneOf[Int]#Or[Double]#Or[String] | |
| def foo[T : TP](t: T) = t | |
| val i: Int = foo(42) | |
| val s: String = foo("foo") | |
| val d: Double = foo(42.4) | |
| //val err: Boolean = foo(true) // doesn't compile | |
| } |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment