julianpeeters

// AVL trees, intrinsically and extrinsically typed

/* "extrinsically typed" AVL trees
 *
 * avlTree : tree -> type.
 * avlTree/leaf : avlTree leaf.
 * avlTree/node-1: avlTree (node L R)
 *   <- height L (s H)
 *   <- height R H.
 * avlTree/node0: avlTree (node L R)

julianpeeters

%Rob Simmons (he) (F2'23)
%9:12 AM
%Patterns of terms/judgments/theorems in a Twelf file

nat: type.           % pattern is "a0 : k0"
z: nat.              % pattern is "c0 : tau"
s: nat -> nat.       % pattern is "c0 : tau"
two : nat = s (s z). % pattern is "c0 : tau = t"

plus : nat -> nat -> nat -> type. % pattern is "a1 : k1"

julianpeeters

sealed trait Nat
case object Zero extends Nat
case class Successor[N <: Nat](nat: N) extends Nat

/* Max, implemented in Twelf, then as a Scala def, and finally as a Scala match types
 * 
 * max : nat -> nat -> nat -> type.
 * %mode max +N1 +N2 -N3.
 * max/z1 : max z N N.
 * max/z2 : max N z N.

julianpeeters

sealed trait Nat
case object Zero extends Nat
case class Successor[A <: Nat](a: A) extends Nat

sealed trait Odd[+N]
case class OddS[N <: Nat](even: Even2[N]) extends Odd[Successor[N]]

sealed trait Even2[+N]
case object Even2Z extends Even2[Zero.type]
case class Even2S[N <: Nat](odd: Odd[N]) extends Even2[Successor[N]]

julianpeeters

sealed trait Nat
case object Zero extends Nat
case class Successor[N <: Nat](nat: N) extends Nat

sealed trait Even[+N]
case object EvenZ extends Even[Zero.type]
case class EvenS[N <: Nat](even: Even[N]) extends Even[Successor[Successor[N]]]

sealed trait Odd[N]
case class OddS[N <: Nat](even: Even2[N]) extends Odd[Successor[N]]

julianpeeters

// Unable to implement `tabulate` without a value to provide as the index
implicit def representableForStore[S]: Representable.Aux[[A] =>> Store[S, A], S] =
  new Representable[[A] =>> Store[S, A]]:
    override type Representation = S
    override val F: Functor[[A] =>> Store[S, A]] = Functor[[A] =>> Store[S, A]]
    override def tabulate[A](f: S => A): Store[S, A] = ???
    override def index[A](f: Store[S, A]): S => A = (s: S) => f.peek(s)

julianpeeters

trait Coercible[A, B] {
  def coerce(a: A): B
}

def coerce[A, B](a: A)(implicit coerceAB: Coercible[A, B]): B = {
  coerceAB.coerce(a)
}

trait Newtype[+T] {
  val value: T

julianpeeters

import cats.effect.{Concurrent, Sync}
import cats.effect.concurrent.{Deferred, Ref}
import cats.effect.implicits._
import cats.implicits._
import scala.collection.mutable.Queue

trait FlushableQueue[F[_], A] {
  def enqueue(a: A): F[Unit]
  def dequeueAll: F[List[A]]
}

julianpeeters

import cats.implicits._
import cats.data._
import cats.effect._
import cats.effect.concurrent._

abstract class Alg[F[_]]{
  def up: F[Unit]
  def down: F[Unit]
  def get: F[Int]
}

julianpeeters

category

arrow
object
  initial object


  A        B        C