scala3-dependent-types-polymorphic-functions-phantom-types-workshop

references

preface

goals of this workshop
- understanding dependent types
  - comprehension how to apply that in practice based on scala3
    - singleton types
    - =:=
    - type level programming
    - polymorphic functions
- applying phantom types to provide compile-time proofs
- understanding path dependent types
  - applying knowledge in practice
- noticing correspondence between logic and computations
  - formal proofs for basic tautologies
  - implemetation of union types using with

workshop plan

pt1_SizedList

context: rust

in rust arrays has compile-time size
- reason: everything allocated on stack must have known size
  - array is allocated on stack
- example: https://play.rust-lang.org/
```
fn main() {
    let array1: [i32; 3] = [1, 2, 3];
    let array2: [i32; 2] = [4, 5];
}
```

what rust can't do (at least - for now) is concatenating of two arrays of different size

reason: no way to perform operations on types, for example: adding them

solution: generic_const

#![allow(incomplete_features)]
#![feature(generic_const_exprs)]

fn concat_arrays<T, const A: usize, const B: usize>(
    a: [T; A], b: [T; B]
) -> [T; A+B]
where
    T: Default,
{
    let mut ary: [T; A+B] = std::array::from_fn(|_| Default::default());
    for (idx, val) in a.into_iter().chain(b.into_iter()).enumerate() {
        ary[idx] = val;
    }
    ary
}

fn main() {
    let array1: [i32; 3] = [1, 2, 3];
    let array2: [i32; 2] = [4, 5];

    let result_array: [i32; 5] = concat_arrays(array1, array2);

    println!("{:?}", result_array);
}

task: implement collection that tracks its size at compile time

use case: allow us to create matrices of a known size and check at compile time that they are multipliable
implement safe version of head (fails compilation if invoked on empty list)

example

rust

example

fn main() {
    let array1: [i32; 0] = [];

    let head = array1[0]; // does not compile: index out of bounds: the length is 0 but the index is 0
}

idris - https://tio.run/#idris

data Vect : Nat -> Type -> Type where
  Nil : Vect Z a
  (::) : a -> Vect n a -> Vect (plus 1 n) a -- (plus 1 n) same as (S n)

concat : Vect n a -> Vect m a -> Vect (n + m) a
concat Nil ys = ys
concat (x :: xs) ys = x :: concat xs ys

head : Vect (plus 1 n) a -> a
head (x :: xs) = x

v0 : Vect 0 a
v0 = Nil
v3 : Vect 3 Integer
v3 = 10 :: 5 :: 1 :: Nil
v4 : Vect 4 Integer
v4 = 1 :: 2 :: 3 :: 4 :: Nil

v3v4 : Vect 7 Integer
v3v4 = concat v3 v4

v3Head : Integer
v3Head = head v3

-- v0Head: Integer
-- v0Head = head v0 -- not compiling, there is no function head for 0-sized vector

main : IO ()
main = putStrLn $ "head of v1: " ++ show v3Head

pt2_SList

implement methods: append and reverse using foldRightF

why normal foldRight is not enough?

notice that in classical foldRight type of accumulator (B) cannot change during processing

trait SList[N <: Int]: // assume that SList has Strings
    def foldRight[B](z: B)(op: (String, B) => B): B

// SList.foldRight(SNil) { case (elem, acc) => SCons(elem, acc) } // not compiles, SNil is SList[0] and SCons is SList[M]

pt3_TypeSafeMethod
- implement type safe version of format that validates arguments based on specified types
  - should support
    - %s -> String
    - %d -> Int
    - any arbitrary combination of them with every cardinality > 1
  - example
```
tsFormat("%s is %d")("s1", 1) // compiles
tsFormat("%s %s %s is %d %s")("s1", "s2", "s3", 1, "s4") // compiles
tsFormat("%s is %d")(i, s) // does not compile: Found: (i : Int) Required: String
```
- explain why cardinality == 1 is complicating a bit implementation
pt4_pathDependent
- rewrite path dependent approach into generics
- discuss variance
pt5_LogicalProofs
- proof theorems:
  1. (all S are M) and (all M are P) => all S are P
  2. (not all S are M) and (all M are P) => not all S are P
pt6_CurryHoward
- using De Morgan's law implement equivalent of sum type: |
- use phantom types to apply that in method's as evidence

prerequisite

summon[T]
- find a given instance of type T in the current scope
=:=
- instance of A =:= B witnesses that the types A and B are equal
- example: proof of being the same type
```
val i = 5 // val i: 5 = 5
summon[i.type =:= 5]
```
<:<
- instance of A <:< B witnesses that A is a subtype of B

phantom types

called this way, because they never get instantiated
- used to represent type relationships rather that working directly with their values
commonly used to express constraints encoded in types
- to prove static properties of the code using type evidences

prevent some code from being compiled in certain situations

useful when representing models that have a particularily defined structural state with transitions

example: assume we need a function that turns a machine on (turnOn), only if it is turned off

sealed trait MachineState
object MachineState {
    sealed trait TurnedOn extends MachineState
    sealed trait TurnedOff extends MachineState
}

case class Machine[State <: MachineState](){
  def open(implicit ev: State =:= Closed) = Door[Open]()
  def close(implicit ev: State =:= Open) = Door[Closed]()
}

are needed only for compilation
- do not come with extra runtime overhead

builder pattern context

example: sql query builder
- problem: aggregation query without group_by will fail
- solution: ZIO SQL
  - https://github.com/zio/zio-sql/blob/b63708a35fb27eeab7a7edf4e320809fce77b5fc/core/jvm/src/main/scala/zio/sql/select/Read.scala#L183

case study: case class builder

problem: verification that all fields are filled

case class Person(firstName: String, lastName: String, email: String)

Person person = new PersonBuilder()
    .firstName("Hello")
    .lastName("World")
    .build(); // email not set, handle situation

solution

naive approach
1. push checks to runtime - throw runtime exception
  - loosing referential transparency
2. build() returns Either[Error, Person]
  - troublesome for caller

phantom types approach

class PersonBuilder[State <: PersonBuilderState] private (
    val firstName: String,
    val lastName: String,
    val email: String) {
  def firstName(firstName: String): PersonBuilder[State with FirstName] =
    new PersonBuilder(firstName, lastName, email)
  def lastName(lastName: String): PersonBuilder[State with LastName] =
    new PersonBuilder(firstName, lastName, email)
  def email(email: String): PersonBuilder[State with Email] =
    new PersonBuilder(firstName, lastName, email)
  def build()(using State =:= FullPerson): Person = // phantom type
    Person(firstName, lastName, email)
}

object PersonBuilder {
  sealed trait PersonBuilderState
  object PersonBuilderState {
    sealed trait Empty extends PersonBuilderState
    sealed trait FirstName extends PersonBuilderState
    sealed trait LastName extends PersonBuilderState
    sealed trait Email extends PersonBuilderState
    type FullPerson = Empty with FirstName with LastName with Email
  }
  def apply(): PersonBuilder[Empty] = new PersonBuilder("", "", "")
}

ZIO environment parameter context is phantom type
- is internally used by ZIO to verify that we have provided all the required environment
  - only programs ZIO[Any, _, _] are executable
- usually there is no type R that user can provide
  - example: ZIO[R1 with R2, E, A]
    - we need to either provide
      1. ULayer[R1], ULayer[R2]
      2. ULayer[R1 with R2]
        
        there is no value R1 with R2

singleton types

"inhabitant of a type" means an expression which has some given type
- example
```
val length: String => Int = (s: String) => s.length
```
usually types has more than one inhabitant
- Boolean: two values
- Int: [Int.MinValue; Int: MaxValue]
- String: infinitely many
notice that there are types that has no values
- type without any value is the "bottom" type
- example: Function1[String, Nothing]

singleton types = types which have a unique inhabitant

examples
- Unit = only one inhabitant
- (a: A, b: B) = |A| x |B| number of inhabitants
- Either(a: A, b: B) = |A| + |B| number of inhabitants
- literal types = type inhabited by a single constant value known at compile-time (literal)
```
val i5: 5 = 5
```
- types inhabited by a single value not known at compile-time
```
val userInput = StdIn.readInt()
val userInput2 = StdIn.readInt()
val iInput: userInput.type = userInput
val iInput2: userInput2.type = userInput // not compiling, compiles only with `= userInput2`
```

bridge the gap between types and values

example: compile-time operations on types

import scala.compiletime.ops.string.*
// type Length[X <: String] <: Int

val a: Length["Hello"] = 5
val b: Length["Hello"] = "Hello".length() // not compiling, length() returns general Int, but we need 5

or for int

import scala.compiletime.ops.int.*
// type +[X <: Int, Y <: Int] <: Int

val result: 5 + 6 = 11

note that operations could be added, suppose that we want to add Read type for strings

import scala.compiletime.ops.string.Read // type we want to add

val a: Read["path/to/some/file"] = "Hello\n"

// 1. go to Dotty core -> Types -> AppliedType -> tryNormalize -> tryCompiletimeConstantFold
// 1. find where types are handled and add additional entry
case tpne.Read => constantFold1(stringValue, scala.io.Source.fromFile(_).mkString)
// 1. add Read name to `tpne` (StdNames)
final val Read: N = "Read"
// 1. add to compiletimePackageStringTypes

Scala 3

Singleton is used by the compiler as a supertype for singleton types
- example
```
summon[42 <:< Singleton]
```
type inference widens singleton types to the underlying non-singleton type
- example
```
summon[(42 & Singleton) <:< Int]
```

when a type parameter has an explicit upper bound of Singleton, the compiler infers a singleton type

example

def singletonCheck5[T <: Singleton](x: T)(using ev: T =:= 5): T = x
val x = singleCheck42(5) // compiles

def typeCheck5[T](x: T)(using ev: T =:= 5): T = x
val x = typeCheck5(5) // not compiles: cannot prove that Int =:= (5 : Int)

are a technique for "faking" dependent types in non-dependent languages
- good approximation of dependent types

bridges the gap in phase separation between runtime values and compile-time types

example

val stdInputLine: String = scala.io.StdIn.readLine()
val inputLine: stdInputLine.type = stdInputLine

allow programmers to use dependently typed techniques to enforce rich constraints among the types
- example: using singletons provably* correct sorting algorithm
  - more accurately, it is a proof of partial correctness
  - * means: sorting algorithm compiles in finite time and when it runs in finite time => result is indeed a sorted list

polymorphic lambda

is a function type which accepts type parameters

example

def reverse[A](xs: List[A]): List[A] = xs.reverse // polymorphic method
val reverse2: [A] => List[A] => List[A] = [A] => (xs: List[A]) => reverse[A](xs) // polymorphic lambda

are not to be confused with type lambdas
- polymorphic lambda describes type of a polymorphic value
  - are applied in terms
    - terms = type inhabitants
      - example
        
        Nothing has 0 terms
        
        Unit has 1 term
        
        Boolean has 2 terms
- type lambda is an actual function value at the type level
  - are applied in types
type lambda
- lets one express a higher-kinded type directly, without a type definition
  - types belong to kinds
    - think of kinds as types of types
    - example
      - Int belongs to 0-level kinds
      - List[_] belongs to 1-level kinds
        
        it takes 0-level kind as type argument
        
        similar to a function: takes a level-0 type and returns a level-0 type
        [X] -> List[X]
- example
  - type definition
    - unparameterized with a type lambda: type T = [X] =>> R
    - parameterized: type T[X] = R
      - shorthand for an unparameterized definition
    - unparameterized with a type lambda: type T = [X] =>> R
- defines a function from types to types
  - type analog of “value lambdas”
- body of a type lambda can again be a type lambda
  - curried type parameters
- before Scala 3, API designers had to resort to compiler plugins, namely kind-projector, to achieve the same level of expressiveness
  - scala2: doesn’t allow us to use underscore syntax to simply say Either[Throwable, _]
```
// type projection implementing the same type anonymously (without a name)
({type L[A] = Either[Throwable, A]})#L
```
  - kind-projector: Either[Throwable, *]
  - scala3: [K] =>> Either[Throwable, K]
    - use case: given Monad[[R] =>> Either[Throwable, R]]

dependent types

gradation
- values depending on values: functions
  - typed lambda calculi: term - term
- values depending on types: polymorphism
```
def twice[A](a: A)(f: A => A): A = f(f(a))
```
- types depending on values: dependent types
- types depending on types: type functions
  - higher order types
dependent type systems: "values may also appear in types"
question of how to enforce invariants has two answers in dependent types
- intrinsic
  - implies that a “wrong” value cannot be constructed at all
  - example
```
-- Agda intrinsic
get :: (xs : List a l) -> Fin l -> a // Fin is a type defined in such a way that it can only take values from 0 up to n - 1
```
- extrinsic
  - allow any input, but then require an additional proof of the fact that input is within constraints
  - more similar to a refinement
  - example
```
-- Agda extrinsic
get :: (xs : List a l) -> (n : Nat) -> (inBounds n l) -> a
```
let you move some checks to the type system itself
- making it impossible to fail while the program is running
use cases
1. multiplying matrices
  - encode matrix size in type and verify if multiply is possible at compile time
2. database queries
  - type of valid queries depends on the "shape" of the database
  - type of the result of a query depends on the query itself
3. communication protocols
  - what answer is valid for what message
4. binary serialization
  - all binary formats are described by dependent types
    - exact meaning and layout of later bytes depend on some earlier bytes
    - example: uncompressed picture
      - starts with the size of the picture, number of color channels, bit depth, alignment; followed by the raw data, whose size and interpretation depends on those parameters

Scala context

type structure cannot be deduced from runtime structure

example: filter in sized vector

def filter(p: A => Boolean): SizedList[???, A] // size depends on runtime application of predicate

path dependent types

Scala unifies concepts from object and module systems
- essential ingredient of this unification is to support objects that contain type members in addition to fields and methods
- to make any use of type members, programmers need a way to refer to them
  - some level of dependent types is required
  - usual notion is that of path-dependent types
path dependent type is a specific kind of dependent type in which the type depends on a path
types which are distinguished by the values which are their prefixes

Aux pattern

example

trait Wrapper {
  type A

  def value: A
}

object Wrapper {

  type Aux[A0] = Wrapper { type A = A0 }
  def apply[A0](a: A0): Wrapper.Aux[A0] =
    new Wrapper {
      type A = A0
      def value: A0 = a
    }
}

val w: Wrapper = Wrapper(1)
val wAux = Wrapper(1) // Wrapper.Aux[Int]
val z = wAux.value + wAux.value // ok
val z = w.value + w.value // compilation fails, type of value is really hidden

use cases

hiding internal state: ZIO Schedule[-Env, -In, +Out]
```
trait Schedule[-Env, -In, +Out] extends Serializable { self =>
  import Schedule.Decision._
  import Schedule._

  type State

  def initial: State
```
- reason: putting state will make it complex
  - state can be really long like window recur every 5 seconds etc
  - we don't need to know what it is to work with schedule
    - exposing it means exposing implementation detail
- why not use trait
  - we want to keep it the same in every referred place
- source: https://github.com/zio/zio/blob/series/2.x/core/shared/src/main/scala/zio/Schedule.scala

type inference & partial application

problem: for generics you can only specify all of them or not specify any of the

trait Joiner[Elem, R] {
    def join(xs: Seq[Elem]): R
}

def doJoin[T, R](xs: T*)(using j: Joiner[T, R]): R = j.join(xs)

given Joiner[CharSequence, String] with {
  override def join(xs: Seq[CharSequence]): String = xs.mkString
}

given Joiner[String, String] with {
  override def join(xs: Seq[String]): String = xs.mkString(",")
}

// for Joiner[Elem, R] you can only specify all of them or not specify any of the
doJoin[CharSequence, String]("a", "b", "c")
doJoin[String, String]("a", "b", "c")
doJoin("a", "b", "c")

use case: some subset of types is uniquely determined by other types

example: ZIO Zippable

source: https://github.com/zio/zio/blob/series/2.x/core/shared/src/main/scala/zio/Zippable.scala

no matter how we zip we should always maintain "flat" structure of tuple

((_, _), _) ~ (_, (_, _)) ~ (_, _, _)

example

val zio1: ZIO[Any, Nothing, Int] = ZIO.succeed(1)
val zio2: ZIO[Any, Nothing, Int] = ZIO.succeed(2)
val zio3: ZIO[Any, Nothing, Int] = ZIO.succeed(3)

val zio1_4: ZIO[Any, Nothing, ((Int, Int), Int)] = zio1 <*> zio2 <*> zio3 // ZIO 1: not flattened tuple
val zio2_4: ZIO[Any, Nothing, (Int, Int, Int)] = zio1 <*> zio2 <*> zio3 // ZIO 2: no tuples nesting

digression: it cannot be resolved systematically

val zio1 = ZIO.succeed(1)
val zio2 = ZIO.succeed((2, 3))
val zio3 = ZIO.succeed(3)

val zio2_4: ZIO[Any, Nothing, (Int, (Int, Int), Int)] = zio1 <*> zio2 <*> zio3 // no implicit for that case

Curry-Howard isomorphism

proposition refers to a statement or assertion that can be either true or false
both logic and programming with functions are built around the notion of hypotheticals
- proposition 𝐴→𝐵 says "if I had an 𝐴, I could prove 𝐵"
- function of type 𝐴→𝐵 says "if I had a value of type 𝐴, I could compute a value of type 𝐵"
- these logics/languages are really systems for hypothetical reasoning, which we need for both programming and proving
- whether we say "prove" or "compute" really just depends on whether we only care about
  - existence of an 𝐵
  - or which 𝐵 we get
propositions as types
- bottom type = logical falsehood
  - Scala’s Nothing type
  - used to define type negation
```
type Not[A] = A => Nothing
```
    - on the logical side of Curry-Howard this maps to A -> false, which is equivalent to ~A
  - polymorphic function absurd[A]: Nothing => A corresponds to statement "from falsehood you can derive everything"
    - it cannot be constructed, but intuitively it is just a promise: if you give me element of nothing I will give you element of A
      - usually called absurd[A]: Nothing => A
      - notice that for any set 𝐴, there is exactly one function from the empty set to 𝐴
        
        graph of an empty function is a subset of the Cartesian product ∅×𝐴
        
        since the product is empty the only such subset is the empty set ∅
- function type = implication
- product type = conjunction
- sum type = disjunction
- inhabited types = provable theorems
  - we cannot implement generic function f: A => B
    - it would mean we can prove implication A -> B - from any information A we can derive any information B
    - to do that, we need some kind of connection between A and B
relates systems of formal logic to models of computation
- propositions as types
  - useful way to think of types is to view them as predictions
    - if the expression terminates, you know what form the expression is
- proofs as programs
  - proof of a proposition is a program of that type
  - provability corresponds to inhabitation
    - if we can find the values that exist for a given a type, it turns out that the type corresponds to a true mathematical theorem
- normalisation of proofs as evaluation of programs
propositional calculus
- implication, negation, conjunction, disjunction, exclusive OR and equality
- problem: doesn’t know about sets, considering just atomic values
first-order logic
- extends propositional logic
  - introduces quantifiers to atomic values
    - Universal quantification ∀
    - Existential quantification ∃
- corresponds to dependent types
  - statement: for all x, if x is a student then x has an ID
```
trait Student { type Id }
```
- is undecidable
  - Gödel’s incompleteness theorem, which says that even in the formal complete system you can come across with unprovable statements
    - example: "this statement is not provable"
      - case 1: this statement is false => it is provable => we proved something that is false
        
        goes agains whole idea of proofs
        
        if you can proove things that are false => logic is not very useful
      - case 2: this statement is true => we have statements that are not provable
second-order logic
- apply quantifiers not only to atomic values but to sets and predicates as well
  - example: there exists a property that holds for all natural numbers greater than 5
    - vs FOL: we can say at most that for property P(x) we have: for all natural numbers greater than 5 P(x) holds
- corresponds to polymorphic types
  - statement: ∃ P : Students → Bool, ∀ s : Students, hasPassed(s) = P(s)
```
trait StudentPredicate[-A] {
  def test(student: A): Boolean
}

def hasPassed[A](student: A)(using predicate: StudentPredicate[A]): Boolean =
  predicate.test(student)
```
has practical implications in e.g. program verification
- example: proof that reverse o reverse == identity
  - by induction and with lemma reverse (xs ++ ys) == reverse ys ++ reverse xs
- formal verification is an automated process that uses mathematical techniques to prove the correctness of the program
  - can prove that program's business logic meets a predefined specification
- formal model is a mathematical description of a computational process
  - provide a level of abstraction over which analysis of a program's behavior can be evaluated
in some sense, the Curry-Howard isomorphism isn't an isomorphism at all
- some people prefer the word "correspondence"
- maybe it's not "two things that are isomorphic" but "two different views of the same thing"

mtumilowicz/scala3-dependent-types-polymorphic-functions-workshop

scala3-dependent-types-polymorphic-functions-phantom-types-workshop

preface

prerequisite

phantom types

singleton types

polymorphic lambda

dependent types

path dependent types

Curry-Howard isomorphism