Skip to content

Commit 630eb03

Browse files
cvogtcvogt
committed
Add type-level boolean algebra and subset tests, improves subtype constraints
1 parent edb5e47 commit 630eb03

File tree

9 files changed

+400
-108
lines changed

9 files changed

+400
-108
lines changed

‎project/Build.scala‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ object MyBuild extends Build{
1616
//scalacOptions ++= Seq("-Xprint:patmat", "-Xshow-phases"),
1717
testOptions in Test += Tests.Argument(TestFrameworks.ScalaTest, "-oFD"),
1818
parallelExecution := false, // <- until TMap thread-safety issues are resolved
19-
version := "0.2-SNAPSHOT",
19+
version := "0.2",
2020
organizationName := "Jan Christopher Vogt",
2121
organization := "org.cvogt",
2222
scalacOptions in (Compile, doc) <++= (version,sourceDirectory in Compile,name).map((v,src,n) => Seq(

‎readme.txt‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,11 @@ scala-extensions: Useful extensions for the Scala standard library
22
http://cvogt.org/scala-extensions/
33

44
Contents:
5+
Type-level constraints (org.cvogt.constraints)
6+
- Comparisons: <:<, =:=, >:>, !=:=, !<:<, !>:>, e.g. String !=:= And
7+
- Boolean Algebra: True, False, ==, !, &&, ||, Implies, Xor
8+
- Subset tests: In, NotIn, e.g. Int NotIn (Any,AnyRef,AnyVal)
9+
510
Collection extensions (org.cvogt.collection)
611
- distinctBy - remove duplicates by key
712
- foldWhile / reduceWhile - stoppable accumulation

‎src/main/scala/constraint.scala‎

Lines changed: 32 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -1,46 +1,40 @@
11
package org.cvogt.scala.constraint
22
import scala.annotation.implicitNotFound
33

4-
/** Verifies that From is NOT a subtype of To */
5-
@implicitNotFound(msg =
6-
"""
7-
Cannot prove that
8-
${From}
9-
is not a subtype of
10-
${To}"""
11-
)
12-
trait !<:[From, To]
13-
object !<:{
14-
/** implicit that verifies !<: */
15-
implicit def conforms_!<:[A,B](implicit ev: Allow_!<:[A, B]): A !<: B = null
4+
import boolean._
5+
6+
/**
7+
type-level constraints for subtyping and type identity checks.
8+
*/
9+
object `package`{
10+
@implicitNotFound(msg = "Cannot prove ${Left} =:= ${Right}")
11+
type =:=[Left,Right] = scala.Predef.=:=[Left,Right]
12+
@implicitNotFound(msg = "Cannot prove ${Left} <:< ${Right}")
13+
type <:<[Left,Right] = scala.Predef.<:<[Left,Right]
14+
15+
@implicitNotFound(msg = """Cannot prove ${Left} !<:< ${Right}""")
16+
type !<:<[Left,Right] = ![<:<[Left,Right]]
17+
@implicitNotFound(msg = """Cannot prove ${Left} !=:= ${Right}""")
18+
type !=:=[Left,Right] = ![=:=[Left,Right]]
19+
20+
21+
@implicitNotFound(msg = """Cannot prove ${Left} >:> ${Right}""")
22+
type >:>[Right,Left] = <:<[Left,Right]
23+
@implicitNotFound(msg = """Cannot prove ${Left} !>:> ${Right}""")
24+
type !>:>[Right,Left] = !<:<[Left,Right]
1625
}
17-
/** Helper class for !<: */
18-
trait Allow_!<:[From, To]
19-
object Allow_!<:{
20-
/** Allow any two types fo !<: */
21-
implicit def allow_!<:[From, To]: Allow_!<:[From, To] = null
22-
/** Creates an ambigious implicit for From <: To to prevent that case. */
23-
implicit def disallow_!<:[From, To](implicit ev: From <:< To): Allow_!<:[From, To] = null
26+
/*
27+
/** Proves that Left is NOT a subtype of ${Right} */
28+
@implicitNotFound(msg = "Cannot prove ${Left} !<:< ${Right}")
29+
final class !<:<[Left, ${Right}]
30+
object !<:<{
31+
implicit def prove[Left,Right](implicit ev: ![Left <:< ${Right}]) = new !<:<[Left,Right]
2432
}
2533
26-
/** Verifies that From is not identical to To */
27-
@implicitNotFound(msg =
28-
"""
29-
Cannot prove that
30-
${From}
31-
is not identical to
32-
${To}"""
33-
)
34-
trait !=:=[From, To]
34+
/** Proves that Left is NOT identical to ${Right} */
35+
@implicitNotFound(msg = "Cannot prove ${Left} !=:= ${Right}")
36+
final class !=:=[Left, ${Right}]
3537
object !=:={
36-
/** implicit that verifies !=:= */
37-
implicit def conforms_!=:=[A,B](implicit ev: Allow_!=:=[A, B]): A !=:= B = null
38-
}
39-
/** Helper class for !=:= */
40-
trait Allow_!=:=[From, To]
41-
object Allow_!=:={
42-
/** Allow any two types fo !=:= */
43-
implicit def allow_!=:=[From, To]: Allow_!=:=[From, To] = null
44-
/** Creates an ambigious implicit for From =:= To to prevent that case. */
45-
implicit def disallow_!=:=[From, To](implicit ev: From =:= To): Allow_!=:=[From, To] = null
38+
implicit def prove[Left,Right](implicit ev: ![Left =:= ${Right}]) = new !=:=[Left,Right]
4639
}
40+
*/

‎src/main/scala/constraint/boolean.scala‎

Lines changed: 66 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,66 @@
1+
package org.cvogt.scala.constraint.boolean
2+
import scala.annotation.implicitNotFound
3+
4+
/** type-level boolean algebra */
5+
object `package`
6+
7+
/** Type representing Boolean True for type-level boolean algebra */
8+
@implicitNotFound(msg = """Cannot prove True. This should never happen. Maybe you have ambiguous implicits.""")
9+
final class True
10+
object True{
11+
implicit def succeed = new True
12+
}
13+
/** Type representing Boolean False for type-level boolean algebra */
14+
@implicitNotFound(msg = """Cannot prove False""")
15+
final class False
16+
17+
/** Proves that Constraint does NOT hold */
18+
@implicitNotFound(msg = """Cannot prove ![${Constraint}]""")
19+
final class ![Constraint]
20+
object !{
21+
implicit def prove[Constraint](implicit ev: Helper_![Constraint]) = new ![Constraint]
22+
}
23+
24+
final class Helper_![Constraint]
25+
object Helper_!{ // For better error message than ambigious implicit
26+
/** Implicit that always succeeds */
27+
implicit def succeed[Constraint] = new Helper_![Constraint]
28+
/** Creates an ambigious implicit if Constraint holds. */
29+
implicit def prove[Constraint](implicit ev: Constraint) = new Helper_![Constraint]
30+
}
31+
32+
/** Proves both Left and Right */
33+
@implicitNotFound(msg = "Cannot prove ${Left} && ${Right}")
34+
final class &&[Left, Right]
35+
object &&{
36+
implicit def prove[Left,Right](implicit ev1: Left, ev2: Right) = new &&[Left,Right]
37+
}
38+
39+
/** Proves Left Implies Right */
40+
@implicitNotFound(msg = "Cannot prove ${Left} Implies ${Right}")
41+
final class Implies[Left, Right]
42+
object Implies{
43+
implicit def prove[Left,Right](implicit ev: ![Left] || Right) = new Implies[Left,Right]
44+
}
45+
46+
/** Proves Left Implies Right */
47+
@implicitNotFound(msg = "Cannot prove ${Left} Implies ${Right}")
48+
final class Xor[Left, Right]
49+
object Xor{
50+
implicit def prove[Left,Right](implicit ev: (Left || Right) && ![Left && Right]) = new Xor[Left,Right]
51+
}
52+
53+
/** Proves or disproves both Left and Right (aka Left ≡ Right, Left <=> Right) */
54+
@implicitNotFound(msg = "Cannot prove ${Left} IdenticalTo ${Right}")
55+
final class ==[Left, Right]
56+
object =={
57+
implicit def prove[Left,Right](implicit ev: ![Left Xor Right]) = new ==[Left,Right]
58+
}
59+
60+
/** Proves either Left or Right */
61+
@implicitNotFound(msg = "Cannot prove ${Left} || ${Right}")
62+
final class ||[Left, Right]
63+
object ||{
64+
implicit def proveLeft[Left,Right](implicit ev: Left) = new ||[Left,Right]
65+
implicit def proveRight[Left,Right](implicit ev: Right && ![Left]) = new ||[Left,Right]
66+
}

‎src/main/scala/constraint/set.scala‎

Lines changed: 45 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,45 @@
1+
package org.cvogt.scala.constraint.set
2+
import scala.annotation.implicitNotFound
3+
import scala.language.higherKinds
4+
5+
import org.cvogt.scala.constraint.boolean._
6+
7+
/** type-level subset tests */
8+
object `package`{
9+
/* abstract over operations, so we can so a strict and a subtyping subset check
10+
type SetOps[Op1[_,_],Op2[_,_]] = {
11+
type In2[Left,T1,T2] = (Left Op1 T1) Op2 (Left Op1 T2)
12+
}
13+
type Ops = SetOps[=:=,||]
14+
*/
15+
}
16+
17+
/** Proves that Left is a component of the tuple given as Right */
18+
@implicitNotFound(msg = "Cannot prove ${Left} In ${Set}")
19+
final class In[Left, Set]
20+
object In{
21+
implicit def prove2[Left,T1,T2](
22+
implicit ev: (Left =:= T1) || (Left =:= T2)
23+
) = new In[Left,(T1,T2)]
24+
25+
implicit def prove3[Left,T1,T2,T3](
26+
implicit ev: (Left =:= T1) || (Left =:= T2) || (Left =:= T3)
27+
) = new In[Left,(T1,T2,T3)]
28+
29+
implicit def prove4[Left,T1,T2,T3,T4](
30+
implicit ev: (Left =:= T1) || (Left =:= T2) || (Left =:= T3) || (Left =:= T4)
31+
) = new In[Left,(T1,T2,T3,T4)]
32+
33+
implicit def prove5[Left,T1,T2,T3,T4,T5](
34+
implicit ev: (Left =:= T1) || (Left =:= T2) || (Left =:= T3) || (Left =:= T4) || (Left =:= T5)
35+
) = new In[Left,(T1,T2,T3,T4,T5)]
36+
}
37+
38+
/** Proves that the first type is NOT a component of the tuple given as the second type */
39+
@implicitNotFound(msg = "Cannot prove ${Left} NotIn ${Set}")
40+
final class NotIn[Left, Set]
41+
object NotIn{
42+
implicit def prove[Left,Set](
43+
implicit ev: ![Left In Set]
44+
) = new NotIn[Left,Set]
45+
}

‎src/test/scala/ConstraintTest.scala‎

Lines changed: 0 additions & 69 deletions
This file was deleted.

‎src/test/scala/constraint.scala‎

Lines changed: 74 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,74 @@
1+
package org.cvogt.test.scala.constraint
2+
3+
import org.scalatest.FunSuite
4+
import org.scalactic.TypeCheckedTripleEquals._
5+
6+
import org.cvogt.scala.constraint._
7+
8+
trait A
9+
trait B extends A
10+
trait C
11+
12+
class ConstraintTest extends FunSuite{
13+
test("<:<"){
14+
implicitly[A <:< A]
15+
implicitly[B <:< A]
16+
implicitly[B <:< B]
17+
implicitly[A >:> A]
18+
implicitly[B !>:> A]
19+
implicitly[B >:> B]
20+
implicitly[C !<:< A]
21+
implicitly[A !>:> C]
22+
assertTypeError("implicitly[B !<:< A]")
23+
assertTypeError("implicitly[A !<:< A]")
24+
}
25+
test("=:="){
26+
implicitly[String =:= String]
27+
implicitly[Int =:= Int]
28+
implicitly[Unit =:= Unit]
29+
implicitly[C =:= C]
30+
implicitly[Any =:= Any]
31+
implicitly[AnyRef =:= AnyRef]
32+
implicitly[AnyVal =:= AnyVal]
33+
implicitly[Nothing =:= Nothing]
34+
35+
assertTypeError("implicitly[String =:= Nothing]")
36+
assertTypeError("implicitly[Int =:= Nothing]")
37+
assertTypeError("implicitly[Unit =:= Nothing]")
38+
assertTypeError("implicitly[C =:= Nothing]")
39+
assertTypeError("implicitly[Any =:= Nothing]")
40+
assertTypeError("implicitly[Nothing =:= String]")
41+
assertTypeError("implicitly[Nothing =:= Int]")
42+
assertTypeError("implicitly[Nothing =:= Unit]")
43+
assertTypeError("implicitly[Nothing =:= C]")
44+
assertTypeError("implicitly[Nothing =:= Any]")
45+
}
46+
test("!=:="){
47+
implicitly[String !=:= Any]
48+
implicitly[String !=:= AnyVal]
49+
implicitly[String !=:= AnyRef]
50+
implicitly[String !=:= Unit]
51+
implicitly[Int !=:= Any]
52+
implicitly[Int !=:= AnyRef]
53+
implicitly[Int !=:= AnyVal]
54+
implicitly[Int !=:= Unit]
55+
implicitly[Unit !=:= Any]
56+
implicitly[Unit !=:= AnyRef]
57+
implicitly[Unit !=:= AnyVal]
58+
59+
assertTypeError("implicitly[String !=:= String]")
60+
assertTypeError("implicitly[Int !=:= Int]")
61+
assertTypeError("implicitly[Unit !=:= Unit]")
62+
assertTypeError("implicitly[Nothing !=:= Nothing]")
63+
64+
implicitly[Unit !=:= Nothing]
65+
implicitly[String !=:= Nothing]
66+
implicitly[Int !=:= Nothing]
67+
implicitly[Nothing !=:= Any]
68+
implicitly[Nothing !=:= AnyRef]
69+
implicitly[Nothing !=:= AnyVal]
70+
implicitly[Nothing !=:= Unit]
71+
implicitly[Nothing !=:= String]
72+
implicitly[Nothing !=:= Int]
73+
}
74+
}

0 commit comments

Comments
 (0)