Tagless Final in F#¶
Tagless Final in F#
module Poly
#nowarn "62"
type repr = obj
let invoke<'r, 'f, 'a> (f: 'f) (x: 'a) =
let m = typeof<'f>.GetMethod("Invoke")
let m = if m.IsGenericMethodDefinition then
m.MakeGenericMethod([| x.GetType() |])
else
m
in m.Invoke(f, [| x |]) :?> 'r
// signature
type 'repr Sym =
abstract member zero : 'repr
abstract member succ : 'repr -> 'repr
type inst(zero: repr, succ: repr -> repr) =
interface repr Sym with
member it.zero = zero
member it.succ x = succ x
// It's not easy to erase the type in F#.
// this implementation works but many other
// equivalent will just fail, e.g., I tried
// to make a `type inst(sym: 'repr Sym) = interface repr Sym`,
// but some very confusing thing occurred and polymorphisms
// got lost.
// I haven't made sure if this is due to value restriction.
let erased : 'repr Sym -> repr Sym = fun orig ->
let zero = orig.zero :> repr
let succ (x: repr) = orig.succ (x :?> _) :> repr
inst(zero, succ) :> _
let (|Erased|) x = erased x
// workaround for lack of HRT, like this in OCaml:
// type sym = { e: 'a. (module SYM with repr = 'a) -> 'a }
type sym(f) =
member it.e<'repr> (Erased sym: 'repr Sym): 'repr =
invoke f sym
// succ of initial algebra
let succ : sym -> sym = fun i ->
let f : repr Sym -> repr = fun (Erased impl) -> impl.succ <| i.e impl
sym f
// zero of initial algebra
let zero : sym =
let f : repr Sym -> repr = fun (Erased impl) -> impl.zero
sym f
// implementation 1
type nat = Nat with
interface int Sym with
member cls.zero = 0
member cls.succ i = i + 1
// implementation 2
type show = Show with
interface string Sym with
member cls.zero = "0"
member cls.succ i = sprintf "%s + 1" i
// things are totally type safe.
module Say =
let hello name =
let a = zero
printfn "zero by nat: %d" <| a.e Nat
let h = succ a
printfn "succ zero by show: %s" <| h.e Show
printfn "succ zero by show: %d" <| h.e Nat
produces
zero by nat:
0
succ zero by show:
0 + 1
succ zero by show:
1