Skip to content

Instantly share code, notes, and snippets.

Keigo Imai keigoi

Block or report user

Report or block keigoi

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
@keigoi
keigoi / .depend
Last active Jan 28, 2017
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 27, 2019
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 *)
You can’t perform that action at this time.