einblicker

interface Func<A, B> {
  B apply(final A arg);
}

abstract class Dir<A, B> {
  public Dir() {}
  abstract public Func<Func<String, A>, Func<String, B>> format();
}

class DLit<A> extends Dir<A, A> {

einblicker

object Formatter {
  sealed abstract class Dir[A] {
    def formatAux: String => A
    def format: A = formatAux.apply("")
  }

  case object E extends Dir[String] {
    def formatAux = identity
  }

einblicker

let dummyVal () = failwith "dummy";;

class virtual ['a] dir (dummy : (unit -> 'a)) = object
  method virtual format_aux : string -> 'a
end;;

class d_end = object
 inherit [string] dir dummyVal
 method format_aux =
  fun out -> out

einblicker

class GaloisField private (val gf_index: Int) {
  private val gf_bit: Int =
    if (gf_index == 4) (1 << 1) | 1
    else if (gf_index == 8) (1 << 4) | (1 << 3) | (1 << 2) | 1
    else sys.error("undefined")

  private val pow_table = Array.fill(256)(0)
  private val root_table = Array.fill(256)(0)

  locally {

einblicker

object RSEncoder {
  def encode(raw_code: Array[Int]) = {
    val gf = GaloisField.a8

    val g_index = Array(
      43, 139, 206, 78, 43, 239, 123, 206, 214,
      147, 24, 99, 150, 39, 243, 163, 136
    )

    val code =

einblicker

module FPStyle =

  [<AbstractClass>]
  type Eq<'A, 'B> private () =
    abstract F : 'A -> 'B
    abstract G : 'B -> 'A
    static member Id<'A>() =
      { new Eq<'A, 'A>() with
        member this.F(x) = x
        member this.G(x) = x }

einblicker

Parameter A : Prop.

Goal (forall X : Prop, (A -> X)) -> (A -> (forall X : Prop, X)).
intros.
apply H.
assumption.
Qed.

Goal (A -> (forall X : Prop, X)) -> (forall X : Prop, (A -> X)).
intros.

einblicker

import scalaz._
import Scalaz._

trait REQUAL[A, B] {
  def apply[C[_, _]](
    x: Forall[({type X[D]=C[D, D]})#X]
  ): C[A, B]
}

einblicker

class Hungry(f: Int => Hungry) {
  def apply(n: Int) = f(n)
}

val f: Hungry = new Hungry(_ => f)

f(0)
f(0)(1)(2)
f(0)(1)(2)(3)(4)(5)

einblicker

Section HungryIsImmutable.

CoInductive hungry := h : (nat -> hungry) -> hungry.

CoFixpoint f := h (fun _ => f).

Definition unH x :=
  match x with
  | h f => f 
  end.