Skip to content

Instantly share code, notes, and snippets.

@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 / Kind.hs
Created Sep 10, 2012
weaker kind-inference in ghc 7.4.1
View Kind.hs
{-# LANGUAGE ScopedTypeVariables, KindSignatures #-}
import Data.Typeable
innerTypeOf :: Typeable a => t a -> TypeRep
innerTypeOf (x :: t a) = typeOf (undefined :: a) -- fail
-- giving a kind explicitly will do
-- innerTypeOf (x :: t (a:: *)) = typeOf (undefined :: a) -- ok
@keigoi
keigoi / tailcall.rs
Created Oct 26, 2012
Rust tail call test
View tailcall.rs
// use tail-call only, but stack overflow occur
fn recur(i : int) {
if i!=0 {
recur(i-1);
}
}
fn main() {
recur(1000000);
}
@keigoi
keigoi / CheckMVar.hs
Created Nov 30, 2012
MVar without deadlock -- initial try
View CheckMVar.hs
{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, TypeOperators #-}
--
-- MVar without deadlock
--
module CheckMVar (Z(Z),S(S),(:<),Nil,ListPos,Get,Set,Session,sreturn,sbind,runSession,inSession,inS,FullMVar,EmptyMVar,newMVar,newEmptyMVar,takeMVar,putMVar) where
import qualified Control.Concurrent as C
-- | type level zero
@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 =
View gist:5887184
{-# LANGUAGE GADTs, FlexibleInstances #-}
module Main where
import Control.Monad
import Control.Monad.RWS.Strict
import Control.Monad.Trans.Error
import Prelude hiding (putChar, getChar)
import qualified System.IO as IO
View Alt.v
Axiom A :Set.
CoInductive Stream := Cons : A -> Stream -> Stream.
Definition head (s:Stream) : A :=
match s with
Cons x _ => x
end.
Definition tail (s:Stream) : Stream :=
match s with
@keigoi
keigoi / segv_stackovfl.ml
Last active Dec 26, 2015
OCaml fails with SEGV instead of exception Stack_overflow
View segv_stackovfl.ml
(*
OCaml fails with SEGV instead of exception Stack_overflow
- by Keigo IMAI <keigo.imai@gmail.com>
ocamlopt -g -thread -I +threads unix.cmxa threads.cmxa segv_stackovfl.ml -o a.out
ulimit -s 8192
./a.out 540000
*)
let rec run_forever x =
@keigoi
keigoi / .depend
Last active Jan 1, 2016
Session type implementation using Janestreet Async
View .depend
session.cmi :
example.cmo : session.cmi
example.cmx : session.cmx
session.cmo : session.cmi
session.cmx : session.cmi
@keigoi
keigoi / STLC.v
Last active Aug 29, 2015
Proving soundness of STLC using autosubst
View STLC.v
(* Proving soundness of STLC using autosubst https://www.ps.uni-saarland.de/autosubst/ *)
Require Import Autosubst MMap.
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
(* our type - only booleans and functions *)