Skip to content

Instantly share code, notes, and snippets.

@mheiber
Created June 13, 2023 11:34
Show Gist options
  • Save mheiber/f3aa0b9ca82a7deabf5b4f75a1f4c713 to your computer and use it in GitHub Desktop.
Save mheiber/f3aa0b9ca82a7deabf5b4f75a1f4c713 to your computer and use it in GitHub Desktop.
(* from https://okmij.org/ftp/ML/first-class-modules/ *)
module Eq = struct
type ('a,'b) eq = Refl of 'a option ref * 'b option ref
let refl () = let r = ref None in Refl (r,r)
let symm : ('a,'b) eq -> ('b,'a) eq = function
Refl (x,y) -> Refl (y,x)
let apply_eq : ('a,'b) eq -> 'a -> 'b = function
Refl (rx,ry) -> fun x ->
rx := Some x;
match !ry with
| Some y -> rx := None; y
| _ -> failwith "Impossible"
let apply_eq' : ('a,'b) eq -> 'a -> 'b = function
Refl _ -> Fun.id
end
open Eq
module Example: sig
type t
val x: t
val eq: (t, int) eq
end = struct
type t = int
let x = 3
let eq : (t, int) eq = refl ()
end
let z: int = apply_eq Example.eq Example.x
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment