halcat0x15a

val result = for {
  i <- 100.set("Hello")
  j <- 100.set("World")
} yield i + j

result.value assert_=== ("HelloWorld", 200)

halcat0x15a

val s = for {
  i <- init[Int]
  _ <- modify[Int](_ |+| 5)
  j <- gets[Int, Int](_ |+| 5)
} yield i |+| j

s ! 0 assert_=== 10

s ! 5 assert_=== 20

halcat0x15a

lazy val f: Kleisli[Option, Int, String] = kleisli(5.shows +>: _.shows.some)

f(5) assert_=== Some("55")

lazy val g: Kleisli[Option, String, Int] = ☆(_.parseInt.toOption)

g("5") assert_=== Some(5)

halcat0x15a

Inductive P : Set :=
    I : P
  | PS : P -> P.

Fixpoint Padd (n m : P) : P :=
  match n with
  | I => PS m
  | PS n' => PS (Padd n' m)
  end.

halcat0x15a

Inductive P : Set :=
    I : P
  | PS : P -> P.

Fixpoint Padd (n m : P) : P :=
  match n with
  | I => PS m
  | PS n' => PS (Padd n' m)
  end.

halcat0x15a

object CoqMain {
object CoqModule {
sealed abstract class Nat
case class Zero() extends Nat
case class Succ(x1: Nat) extends Nat
def nat_rect[A] : (A => ((Nat => (A => A)) => (Nat => A))) = {
(f:A) => (f0:(Nat => (A => A))) => (n:Nat) =>
n match {
case Zero() => f
case Succ(n0) => f0(n0)(nat_rect(f)(f0)(n0))

halcat0x15a

trait Nat {
  type Plus[N <: Nat] <: Nat
  def +[N <: Nat](n: N): Plus[N]
  type Mult[N <: Nat] <: Nat
  def *[N <: Nat](n: N): Mult[N]
  def toInt: Int
}

case object Zero extends Nat {
  type Plus[N <: Nat] = N

halcat0x15a

sealed trait SList {
  type Self <: SList
  type Function[A]
  def apply[A](f: Function[A]): A
  def ::[A](a: A) = SCons(a, this.asInstanceOf[Self])
}

case object SNil extends SList {
  type Self = SNil.type
  type Function[A] = A

halcat0x15a

(defprotocol Action
  (action [this e]))

(deftype Controller [^{:unsynchronized-mutable true} label]
  Action
  (action [this e]
    (.setText label "Action!")))

halcat0x15a

trait Foo

type Bar = Int @@ Foo