Skip to content

Instantly share code, notes, and snippets.

View rectype.ts
type Global = {[L:string]:Local}
type Local = {kind:string; role:string, bra:{[L:string]:Local}}
type Keys<T extends {[L:string]:{}}> = T extends infer U ? keyof U : never;
type Assoc<T extends {[L:string]:{}}, K extends string> = T extends unknown ? K extends keyof T ? T[K] : never : never;
type Force<T extends Local> =
[T] extends [Local]
? {kind:T["kind"], role:T["role"], bra:{[X in Keys<T["bra"]>]: Force<Assoc<T["bra"], X>>}}
: never
type Comm<R1 extends XS, R2 extends XS, XS extends string, T extends {[L:string]:Global}> =
@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> {
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);
View mpst.ml
module type S = sig
type _ mpst
type _ sess
type (_, _, _, _) lens
type (_, _) label
type (_, _, _, _) dlabel
type ('a, 'b, 'c, 'd, 'e, 'f) role = ('a, 'b, 'c, 'd) lens * ('e, 'f) label
type _ typ
View Android_Studio_project_on_network_drive.md