emiflake

namespace RFC where
  parseDigit = oneOfChars [?0, ?1, ?2, ?3, ?4, ?5, ?6, ?7, ?8, ?9]
  parseHex = Unipar.satisfy isHexDigit "wasn't a hex digit"
  parseCRLF = (ch ?\r Unipar.>> ch ?\n)

type RawHeaders
  = RawHeaders (Map Text Text)

type Request
  = Request HostName Text RawHeaders

kubukoz

let Rule
    : Type
    = ∀(_Rule : Type) →
      ∀(One : _Rule) →
      ∀(Two : _Rule) →
      ∀(Many : List _Rule → _Rule) →
        _Rule

let example
    : Rule

pchiusano

-- Ability to range over all the elements of a list
ability Each where
  each : [a] -> a

-- Implementation detail - standard early termination ability
ability Abort where abort : x

-- Here's a first usage. `each` lets us traverse multiple lists 
-- elementwise, matching up values at corresponding indices.
> handle 

umazalakain

object LambdaCalculus {
  sealed trait Type
  case class Arrow[S <: Type, T <: Type]() extends Type
  case class Base() extends Type

  sealed trait Ctx
  case class Nil() extends Ctx
  case class Cons[X <: Type, XS <: Ctx]() extends Ctx

umazalakain

object DeBruijn {
  sealed trait Nat
  sealed trait Z           extends Nat
  sealed trait S[n <: Nat] extends Nat

  sealed trait Fin[n <: Nat]
  case class FZ[n <: Nat]()           extends Fin[S[n]]
  case class FS[n <: Nat](n : Fin[n]) extends Fin[S[n]]

  val here : Fin[S[S[Z]]] = FZ()