keigoi

(* compile with ppx_implicits 0.2.0 *)
(* ocamlfind ocamlc -c -package ppx_implicits implicit_read.ml *)
module Read = struct
  type 'v t = (string -> 'v option, [%imp Instances]) Ppx_implicits.t
                 
  let read ?(d:'v t option) x = Ppx_implicits.imp ?d x
end

module Instances = struct
  let _int : string -> int option = fun s ->

keigoi

foobar

keigoi

module Channel : sig
  type 'a t
  type _ gen = SendG : [`send of 'a] gen | RecvG : [`recv of 'a] gen
  type 'a u = U                                       
  (* val send : [`send of 'a] t -> 'a -> unit *)
  (* val receive : [`recv of 'a] t -> 'a *)
  (* val create : 'b u -> ([<`send of 'b | `recv of 'b] as 'a) gen -> 'a t *)
end = struct
  type _ t = Send : 'a Event.channel -> [`send of 'a] t | Recv : 'a Event.channel -> [`recv of 'a] t
  (* type 'a t = 'a Event.channel *)

keigoi

(* subtraction on church numerals in Coq *)
Set Printing Universes.
  
(* we always use universe polymorphism, which is later required to define subtraction *)
Polymorphic Definition church : Type := forall X:Type, (X->X) -> (X->X).

Polymorphic Definition zero : church := fun X s z => z.
Polymorphic Definition suc : church -> church := fun n X s z => s (n X s z).

(* as usual *)

keigoi

package session;

import java.util.function.Function;
import java.util.function.Supplier;

/**
 * Proof-of-concept implementation of session types (including delegation and
 * recursion) in Java. Session channels are assigned on slots _0, _1, _2, etc.
 * This is WIP; no accept/connect. A type Proc<Cons<C0,Cons<C1,..>>> means that
 * process uses session channel at _0 as C0, _1 as C1, ...

keigoi

abstract sig Digit {}
one sig One, Two, Three, Four, Five, Six, Seven, Eight, Nine extends Digit {}

sig Cell {
  content: Digit,
  adjacent : set Cell
}

abstract sig Group {
  cells: set Cell

keigoi

(* try this with 4.02.0+modular-implicits *)
module type Show = sig
  type t
  val show : t -> string
end

implicit module Lam{X:Show} = struct
  type t = [`Var of string | `App of X.t * X.t | `Abs of string * X.t]
  let show : t -> string = function
      |`Var(x) -> x

keigoi

import java.util.function.Consumer;
import java.util.ArrayList;

public class TypeError {


    public static <A> void let(A a, Consumer<A> f)  {
	f.accept(a);
    }

keigoi

class IxMonad<X,Y,T>(val x:T) {}

class Cons<HD,TL>(val hd : HD, val tl : TL) {}
class Nil();

fun <X,Y,T> ret(x: T) : IxMonad<X,Y,T> {
    return IxMonad<X,Y,T>(x)
}

fun <T> run(m : IxMonad<Nil,Nil,T>) : T {

keigoi

# A monad in Crystal
class Id(T)
  getter :value
  
  def initialize(@value : T)
  end

  def bind(&x : T -> Id(U)) forall U
    yield @value
  end