Initial commit

Author: mtumilowicz

.gitignore

@@ -0,0 +1,6 @@
+# Project exclude paths
+/project/project/target/
+/project/target/
+/target/
+/target/scala-3.4.0/classes/
+/target/scala-3.4.0/test-classes/

README.txt

@@ -0,0 +1,4 @@
+* https://github.com/milessabin/strangeloop-2013/tree/master
+* ["Scala vs Idris: Dependent types, now and in the future" by Miles Sabin and Edwin Brady (2013)](https://www.youtube.com/watch?v=fV2no1Rkzdw)
+* https://github.com/mbovel/scalacon-typelevel-operations
+* [Type level Programming in Scala - Matt Bovel](https://www.youtube.com/watch?v=B7uficxARKM)

build.sbt

@@ -0,0 +1,14 @@
+ThisBuild / version := "0.1.0-SNAPSHOT"
+
+ThisBuild / scalaVersion := "3.4.0"
+
+lazy val root = (project in file("."))
+  .settings(
+    name := "scala3-dependent-types-workshop"
+  )
+
+// Add ScalaCheck dependency
+libraryDependencies += "org.scalacheck" %% "scalacheck" % "1.17.0" % Test
+
+// Optional: If you want to use ScalaTest as well
+libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.17" % Test

project/build.properties

@@ -0,0 +1 @@
+sbt.version = 1.9.9

src/main/scala/workshop/CompileTimeSizedVector.scala

@@ -0,0 +1,5 @@
+package workshop
+
+object CompileTimeSizedVector {
+
+}

src/main/scala/workshop/SafeHead.scala

@@ -0,0 +1,5 @@
+package workshop
+
+object SafeHead {
+
+}

src/main/scala/workshop/TypeSafePrintf.scala

@@ -0,0 +1,20 @@
+package workshop
+
+import scala.compiletime.ops.int.{+}
+import scala.compiletime.ops.string.{CharAt, Length, Substring}
+
+object TypeSafePrintf {
+
+  type ArgTypes[S <: String] <: Tuple = S match
+    case "" => EmptyTuple
+    case _ =>
+      CharAt[S, 0] match
+        case '%' =>
+          CharAt[S, 1] match
+            case 'd' => Int *: ArgTypes[Substring[S, 2, Length[S]]]
+            case 's' => String *: ArgTypes[Substring[S, 2, Length[S]]]
+        case _ => ArgTypes[Substring[S, 1, Length[S]]]
+
+  def printf(s: String)(t: ArgTypes[s.type]): Unit = ()
+
+}

src/test/scala/TypeSafePrintfPropertiesSpec.scala

@@ -0,0 +1,59 @@
+import org.scalacheck.Properties
+import org.scalacheck.Prop.forAll
+import org.scalatest.Assertions.{assertCompiles, assertDoesNotCompile}
+import org.scalatest.flatspec.AnyFlatSpec
+import org.scalatest.matchers.should.Matchers
+import workshop.TypeSafePrintf._
+
+
+object TypeSafePrintfPropertiesSpec extends Properties("TypeSafePrintf")  {
+
+  property("supports %s %d format") = forAll { (s: String, i: Int) =>
+    printf("%s is %d")(s, i)
+    true
+  }
+
+  property("support %d %s format") = forAll { (s: String, i: Int) =>
+    printf("%d is %s")(i, s)
+    true
+  }
+}
+
+class TypeSafePrintfSpec extends AnyFlatSpec with Matchers {
+
+  it should "represent %s %s as (String, String)" in {
+    assertCompiles("summon[ArgTypes[\"%s %s\"] =:= (String, String)]")
+  }
+
+  it should "represent %s %s %s as (String, String, String)" in {
+    assertCompiles("summon[ArgTypes[\"%s %s %s\"] =:= (String, String, String)]")
+  }
+
+  it should "represent %s %d as (String, Int)" in {
+    assertCompiles("summon[ArgTypes[\"%s is %d\"] =:= (String, Int)]")
+  }
+
+  it should "represent %d %s as (Int, String)" in {
+    assertCompiles("summon[ArgTypes[\"%d is %s\"] =:= (Int, String)]")
+  }
+
+  it should "compile %s %d format with correctly ordered params" in {
+    assertCompiles("printf(\"%d is %s\")(5, \"a\")")
+  }
+
+  it should "not compile %s %d format with wrong ordered params" in {
+    assertDoesNotCompile("printf(\"%s %d\")(5, \"a\")")
+  }
+
+  it should "not compile %d %s format with wrong ordered params" in {
+    assertDoesNotCompile("printf(\"%d %s\")(\"a\", 5)")
+  }
+
+  it should "not compile %d %s format with too many params" in {
+    assertDoesNotCompile("printf(\"%s %d\")(\"a\", 5, 6)")
+  }
+
+  it should "not compile %d %s format with too few params" in {
+    assertDoesNotCompile("printf(\"%s %d\")(\"a\")")
+  }
+}