4 people like it.
Like the snippet!
HLists, Peano & Typelevel computations
An experiment on typelevel computations.
1:
2:
3:
4:
5:
6:
7:
8:
9:
10:
11:
12:
13:
14:
15:
16:
17:
18:
19:
20:
21:
22:
23:
24:
25:
26:
27:
28:
29:
30:
31:
32:
33:
34:
35:
36:
37:
38:
39:
40:
41:
42:
43:
44:
45:
46:
47:
48:
49:
50:
51:
52:
53:

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<int,HCons<char,HCons<string,HCons<bool,HNil>>>>
let result = (Append $ first) second // HCons (1,HCons ('1',HCons ("1",HCons (true,HNil))))
// length : Succ<Succ<Succ<Succ<Zero>>>>
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

Multiple items
union case HNil.HNil: HNil

type HNil =
 HNil
interface HList
static member ( * ) : f:'a * HNil:HNil > '_arg5 (requires member ( $ ))
Full name: Script.HNil
val f : 'a (requires member ( $ ))
type HList
Full name: Script.HList
Multiple items
union case HCons.HCons: 'a * 'b > HCons<'a,'b>

type HCons<'a,'b (requires 'b :> HList)> =
 HCons of 'a * 'b
interface HList
static member ( * ) : f:'a0 * HCons<'b1,'c> > '_arg8 (requires member ( $ ) and 'c :> HList)
Full name: Script.HCons<_,_>
val f : 'a (requires member ( $ ) and 'c :> HList)
val x : 'b
val xs : #HList
type Peano
Full name: Script.Peano
Multiple items
union case Zero.Zero: Zero

type Zero =
 Zero
interface Peano
static member ( * ) : f:'a * Zero:Zero > '_arg5 (requires member ( $ ))
Full name: Script.Zero
Multiple items
union case Succ.Succ: 'a > Succ<'a>

type Succ<'a (requires 'a :> Peano)> =
 Succ of 'a
interface Peano
static member ( * ) : f:'a0 * Succ<'b> > '_arg8 (requires member ( $ ) and 'b :> Peano)
Full name: Script.Succ<_>
val f : 'a (requires member ( $ ) and 'b :> Peano)
val x : #Peano
type Bool
Full name: Script.Bool
Multiple items
union case True.True: True

type True =
 True
interface Bool
Full name: Script.True
type False =
 False
interface Bool
Full name: Script.False
Multiple items
union case False.False: False

type False =
 False
interface Bool
Full name: Script.False
val head : 'a
val tail : #HList
Multiple items
union case Append.Append: Append

type Append =
 Append
static member ( $ ) : Append:Append * HNil:HNil > ('a > 'a)
static member ( $ ) : Append:Append * HCons<'a,'b> > ('c > HCons<'a,'d>) (requires 'b :> HList and member ( * ) and 'd :> HList)
Full name: Script.Append
val id : x:'T > 'T
Full name: Microsoft.FSharp.Core.Operators.id
val x : 'a
val xs : 'b (requires 'b :> HList and member ( * ) and 'd :> HList)
Multiple items
val list : 'c

type 'T list = List<'T>
Full name: Microsoft.FSharp.Collections.list<_>
Multiple items
union case Length.Length: Length

type Length =
 Length
static member ( $ ) : Length:Length * HNil:HNil > Zero
static member ( $ ) : Length:Length * HCons<'a,'b> > Succ<'_arg7> (requires 'b :> HList and member ( * ) and '_arg7 :> Peano)
Full name: Script.Length
val xs : 'b (requires 'b :> HList and member ( * ) and '_arg7 :> Peano)
Multiple items
union case Even.Even: Even

type Even =
 Even
static member ( $ ) : Even:Even * Zero:Zero > True
static member ( $ ) : Even:Even * Succ<'b> > '_arg11 (requires 'b :> Peano and member ( * ))
Full name: Script.Even
val x : 'b (requires 'b :> Peano and member ( * ))
Multiple items
union case Odd.Odd: Odd

type Odd =
 Odd
static member ( $ ) : Odd:Odd * Zero:Zero > False
static member ( $ ) : Odd:Odd * Succ<'a> > '_arg14 (requires 'a :> Peano and member ( * ))
Full name: Script.Odd
val x : 'a (requires 'a :> Peano and member ( * ))
val first : HCons<int,HCons<char,HNil>>
Full name: Script.first
val second : HCons<string,HCons<bool,HNil>>
Full name: Script.second
val result : HCons<int,HCons<char,HCons<string,HCons<bool,HNil>>>>
Full name: Script.result
val length : Succ<Succ<Succ<Succ<Zero>>>>
Full name: Script.length
More information