Skip to content

Instantly share code, notes, and snippets.

Avatar

Keigo Imai keigoi

View GitHub Profile
@keigoi
keigoi / nested_bogus.ts
Created Oct 15, 2020
TypeScript strange behaviour in nested conditional types
View nested_bogus.ts
type GetFoo<T> = [T] extends [{foo:infer R}] ? R : never;
type Foo = GetFoo<{foo:"A"}> // "A"
type GetFoo0<T> = [T] extends [{foo:string}] ? [T] extends [{foo:infer R}] ? R : never : never;
type Bogus = GetFoo0<{foo:"A"}> // unknown ???
// to remedy this, use indexed type T["foo"]
@keigoi
keigoi / equal.ts
Created Oct 13, 2020
TypeScript type equality and union types
View equal.ts
// returns the intersection of all elements in the union T
// i.e. ToIntersect<T1 | T2 | .. | Tn> = T1 & T2 & .. & Tn
type ToIntersect<T> = (T extends unknown ? (x:T) => void : never) extends (x:infer U) => void ? U : never;
// check if T and U are equal
// Here, ([T] extends [U] ? _ : _) suppresses union distribution.
// See: https://github.com/microsoft/TypeScript/issues/29368
type Eq<T,U> = [T] extends [U] ? [U] extends [T] ? true : false : false;
// check if all elements in the union LS are equal by using (T & U) = (T | U) iff T = U
@keigoi
keigoi / DualWork.java
Last active Sep 20, 2020
Session Type Duality in Java
View DualWork.java
import java.util.function.Consumer;
import java.util.function.Function;
public class DualWork {
// セッション型
public static class End{
public End() {}
public void close() {}
}
public static class Send<CONT> {
@keigoi
keigoi / .depend
Last active Jun 6, 2020
session type in ocaml (proof-of-concept impl.)
View .depend
channel.cmi :
mVar.cmi :
monitor.cmi :
session.cmi :
channel.cmo : monitor.cmi channel.cmi
channel.cmx : monitor.cmx channel.cmi
example.cmo : session.cmi
example.cmx : session.cmx
mVar.cmo : monitor.cmi mVar.cmi
mVar.cmx : monitor.cmx mVar.cmi
@keigoi
keigoi / coroutine.ml
Last active Jun 6, 2020
Coroutine implementation in OCaml, with Oleg's delimited continuation. see http://okmij.org/ftp/continuations/implementations.html#caml-shift
View coroutine.ml
(* Coroutine implementation in OCaml, with Oleg's delimited continuation *)
(* see http://okmij.org/ftp/continuations/implementations.html#caml-shift *)
module D = Delimcc
(* Coroutine yielded a value of type 'a, and will resume with some value of type 'b *)
type ('a, 'b) suspend =
| Cont of 'a * ('b, ('a,'b) suspend) D.subcont
| Finish
let start_coroutine f =
@keigoi
keigoi / subtract_church.v
Last active Apr 11, 2020
subtraction on church numerals in Coq
View subtract_church.v
(* 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 *)
View covid_link_db.cypher
@keigoi
keigoi / README.md
Last active Nov 22, 2019
Scribble parallel loop example
View README.md

Scribble parallel loop example

@keigoi
keigoi / lens.ts
Last active Nov 9, 2018
lens typescript
View lens.ts
function id<A>(x:A): A {
return x;
}
abstract class Lens<V1, V2, S1, S2> {
abstract get(s: S1): V1;
abstract put(s: S1, v:V2) : S2
}
@keigoi
keigoi / adder_protocol.ml
Created Oct 21, 2018
Channel vector generation from Scribble protocol
View adder_protocol.ml
(*
module fase16.adder.Adder;
type <ocaml> "int" from "stdlib" as Int;
global protocol Adder(role C, role S)
{
choice at C
{
Add(Int, Int) from C to S;
Res(Int) from S to C;
do Adder(C, S);
You can’t perform that action at this time.