type HList = interface end and HNil = HNil with static member inline (|*|) (f, HNil) = f $ HNil interface HList and HCons<'a, 'b when 'b :> HList> = HCons of 'a * 'b with static member inline (|*|) (f, HCons(x, xs)) = f $ HCons(x, xs) interface HList type Peano = interface end and Zero = Zero with static member inline (|*|) (f, Zero) = f $ Zero interface Peano and Succ<'a when 'a :> Peano> = Succ of 'a with static member inline (|*|) (f, Succ(x)) = f $ Succ(x) interface Peano type Bool = interface end and True = True with interface Bool and False = False with interface Bool let inline (^+^) head tail = HCons(head, tail) // Examples type Append = Append with static member ($) (Append, HNil) = id static member inline ($) (Append, HCons(x, xs)) = fun list -> HCons (x, (Append |*| xs) list) type Length = Length with static member ($) (Length, HNil) = Zero static member inline ($) (Length, HCons(x, xs)) = Succ (Length |*| xs) type Even = Even with static member ($) (Even, Zero) = True static member inline ($) (Even, Succ (x)) = Odd |*| x and Odd = Odd with static member ($) (Odd, Zero) = False static member inline ($) (Odd, Succ (x)) = Even |*| x let first = 1 ^+^ '1' ^+^ HNil let second = "1" ^+^ true ^+^ HNil // result : HCons>>> let result = (Append $ first) second // HCons (1,HCons ('1',HCons ("1",HCons (true,HNil)))) // length : Succ>>> let length = Length $ result // Succ (Succ (Succ (Succ Zero))) let _ : True = Even $ length // ok let _ : False = Even $ length // type error let _ : True = Odd $ length // type error let _ : False = Odd $ length // ok