 4 people like it.

# HLists, Peano & Type-level computations

An experiment on type-level 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>>> 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 ``````
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

 Link: http://fssnip.net/d2 Posted: 6 years ago Author: Nick Palladinos Tags: hlist , type-level computations