Skip to content

Instantly share code, notes, and snippets.

View bracevac's full-sized avatar

Oliver Bračevac bracevac

  • Former Research Engineer at Galois. Incoming staircase builder.
View GitHub Profile
@bracevac
bracevac / keybase.md
Created March 27, 2020 20:22
keybase

Keybase proof

I hereby claim:

  • I am bracevac on github.
  • I am betareduction (https://keybase.io/betareduction) on keybase.
  • I have a public key ASBRKqoNHBG3FV5ZgTujzO6w66ChYbU2nlVfr-5leJ1Ppwo

To claim this, I am signing this object:

@bracevac
bracevac / tagless_joins.scala
Last active March 14, 2019 13:28
Polyvariadic joins in tagless final. Executable in a recent Scala REPL.
import scala.language.higherKinds
//Module signatures become traits/interfaces
trait Symantics {
type Ctx[A]
type Var[A]
type Repr[A]
type Shape[A]
def from[A](shape: Repr[Shape[A]]): Var[Repr[A]]
type _ trep = ..
type _ trep +=
| TInt: int trep
| TString: string trep
| TFloat: float trep
| TList: 'a trep -> 'a list trep
| TFun: ('a trep * 'b trep) -> ('a -> 'b) trep
(* Emulating type classes *)
module ShowClass = struct
@bracevac
bracevac / tagless_effects_interp.ml
Last active September 3, 2018 15:21
Final tagless interpreters in terms of effects and handlers
(* Encoding tagless interpreters with effects and handlers.
TODOs:
- do more examples from the tagless papers, especially with phantom types
- examples of "higher order transformations", e.g., index-based definitions and index conversions
*)
module NumAlg = struct
(* New symantics instances should extend this. Having this GADT makes it not
truly "tagless". However, many other advantages of the final tagless style
carry over still. Perhaps one could try to improve the theory of effect handlers/handling
@bracevac
bracevac / localization.ml
Created May 2, 2018 09:16 — forked from andrejbauer/localization.ml
Experiments in using multicore OCaml effects to simulate dynamically created local effects.
(** * General support for creation of dynamic effects *)
(** We show how to use the multicore Ocaml effects to dynamically generate local
effects. Such effects are akin to the Eff resources, and they can be used to
implement ML references.
The code is based on "Eff directly in OCaml" by Oleg Kiselyov and KC
Sivaramakrishnan (http://kcsrk.info/papers/caml-eff17.pdf). It was written by
Andrej Bauer, Oleg Kiselyov, and Stephen Dolan at the Dagstuhl seminar
"Algebraic Effect Handlers go Mainstream". *)
@bracevac
bracevac / segfault.ml
Last active December 15, 2017 16:07
Segfaulting Multicore OCaml example
module Segfault = struct
module Nondet = struct
effect Fork : bool
let fork () = perform Fork
let rec forkEach f = function
| [] -> ()
| x::xs ->
(* if branches are swapped, then no segfault occurs *)

Keybase proof

I hereby claim:

  • I am bracevac on github.
  • I am betareduction (https://keybase.io/betareduction) on keybase.
  • I have a public key ASAdkh-1oR4BLWZson8DBibUGXlp41j2XgFSxE_g4QdhXAo

To claim this, I am signing this object: