F# で型レベルプログラミング

[<Struct>]
type Ty<'Type> =
  override __.ToString() =  // 型の表示用
    typeof<'Type>.ToString()
                 .Replace("FSI_0001+", "")
                 .Replace("[", "<")
                 .Replace("]", ">")
                 .Replace("`1", "")
                 .Replace("`2", "")

let inline ty< ^Type > : Ty< ^Type > = Ty()

type True = True with
  static member inline eval (_: Ty<True>) = ty<True>

type False = False with
  static member inline eval (_: Ty<False>) = ty<False>

let inline eval (x: Ty< ^A >) : Ty< ^B > =
  (^A: (static member inline eval: Ty< ^A > -> Ty< ^B >) x)

let true_ = eval ty<True>
true_ |> printfn "%A" // True

let false_ = eval ty<False>
false_ |> printfn "%A" // False

type True with
  static member inline ifThenElse (_: Ty<True>, x, y) = x 

type False with
  static member inline ifThenElse (_: Ty<False>, x, y) = y

type Not<'a> = Not of 'a with
  static member inline eval (_: Ty<Not< ^A >>) : Ty< ^B >
    when ^A: (static member eval: Ty< ^A > -> Ty< ^Bool >) = // (1)
    (^Bool: (static member ifThenElse: Ty< ^Bool > * _ * _ -> Ty< ^B >) ty< ^Bool >, ty<False>, ty<True>) // (2)

let notTrue = eval ty<Not<True>>
notTrue |> printfn "%A" // False

let notNotTrue = eval ty<Not<Not<True>>> // 先に中身を eval するので入れ子も OK
notNotTrue |> printfn "%A" // True

// let error1 = eval ty<Not<bool>>
// ^ error FS0001: The type 'bool' does not support the operator 'eval'

type BadType = BadType with
  static member eval (_: Ty<BadType>) = ty<BadType>

// let error2 = eval ty<Not<BadType>>
// ^ error FS0001: The type 'BadType' does not support the operator 'ifThenElse'

type And<'a, 'b> = And of 'a * 'b with
  static member inline eval (_: Ty<And< ^A, ^B >>) : Ty< ^C >
    when ^A: (static member eval: Ty< ^A > -> Ty< ^A' >)
     and ^B: (static member eval: Ty< ^B > -> Ty< ^B' >) =
    (^A': (static member ifThenElse: _*_*_ -> Ty< ^C >) ty< ^A' >,ty< ^B' >,ty<False>)

type Or<'a, 'b>  = Or of 'a * 'b with
  static member inline eval (_: Ty<Or< ^A, ^B >>) : Ty< ^C >
    when ^A: (static member eval: Ty< ^A > -> Ty< ^A' >)
     and ^B: (static member eval: Ty< ^B > -> Ty< ^B' >) =
    (^A': (static member ifThenElse: _*_*_ -> Ty< ^C >) ty< ^A' >,ty<True>,ty< ^B' >)

let x = eval ty<And<Not<False>, Or<Not<True>, True>>>
// not false && (not true || true)
x |> printfn "%A" // True

type IfThenElse<'_bool, 'a, 'b> = IfThenElse of '_bool * 'a * 'b with
  static member inline eval (_: Ty<IfThenElse< ^X, ^A, ^B>>) : Ty< ^EvalAorB >
    when ^X: (static member eval: Ty< ^X > -> Ty< ^Bool >) =
    (^Bool: (static member ifThenElse: _*_*_ -> Ty< ^EvalAorB >) ty< ^Bool >,eval ty< ^A >,eval ty< ^B >)
    // 制約に絡まないなら eval は値レベルでやってもよい

// 適当な型定数
type A = A with static member eval _ = ty<A>
type B = B with static member eval _ = ty<B> 

type Code = 
  IfThenElse<
    Or<
      Not<True>,
      IfThenElse<
        Or<
          Not<True>, False>,
        BadType, Not<False>>>, // それぞれの型の一致は見ない。どうせ静的に決まる
    A, B>

let result = eval ty<Code>
result |> printfn "%A" // A

type Z = Z with
  static member eval (x: Ty<Z>) = x
  static member inline add (_: Ty<Z>, y) = eval y

type S<'n> = S of 'n with
  static member inline eval (_: Ty<S< ^N >>) : _
    when ^N: (static member eval: Ty< ^N > -> Ty< ^N' >) = ty<S< ^N' >>
  static member inline add (_: Ty<S< ^X >>, _: Ty< ^Y >) : _
    when ^X: (static member eval: Ty< ^X > -> Ty< ^X' >)
     and ^X': (static member add: Ty< ^X' > * Ty< ^Y > -> Ty< ^Z >) =
    ty<S< ^Z >>

type Add<'x, 'y> = Add of 'x * 'y with
  static member inline eval (_: Ty<Add< ^X, ^Y>>) : _
    when ^X: (static member eval: Ty< ^X > -> Ty< ^X' >) =
    (^X': (static member add: _*_ -> _) ty< ^X' >,ty< ^Y >)

type One = S<Z>
type Three = Add<One, Add<One, One>>
type Five = S<Add<Three, One>>

let five = eval ty<Five>
five |> printfn "%A" // S<S<S<S<S<Z>>>>>

type Z with
  static member inline sub (x, _: Ty<Z>) = eval x

type S<'n> with
  static member inline sub (_: Ty<S< ^X> >, _: Ty<S< ^Y >>) : _
    when ^X: (static member eval: Ty< ^X > -> Ty< ^X' >)
     and ^Y: (static member eval: Ty< ^Y > -> Ty< ^Y' >)
     and ^Y': (static member sub: Ty< ^X' > * Ty< ^Y' > -> Ty< ^Z >) =
    ty< ^Z >

type Sub<'x, 'y> = Sub of 'x * 'y with
  static member inline eval (_: Ty<Sub< ^X, ^Y>>) : _
    when ^X: (static member eval: Ty< ^X > -> Ty< ^X' >)
     and ^Y: (static member eval: Ty< ^Y > -> Ty< ^Y' >) =
    (^Y': (static member sub: _*_ -> _) ty< ^X' >,ty< ^Y' >)

type Two = Sub<Three, One>
type Six = Sub<Add<Five, Two>, One>

let six = eval ty<Six>
six |> printfn "%A" // S<S<S<S<S<S<Z>>>>>>

// let error = eval ty<Sub<Two, Six>>
// ^ Type constraint mismatch. The type 'Ty<Z>' is not compatible with type 'Ty<S<'a>>'

type Z with
  static member inline gt (_: Ty<S<_>>, _: Ty<Z>) = ty<True>
  static member inline gt (_: Ty<Z>, _) = ty<False>

type S<'n> with
  static member inline gt (_: Ty<S< ^X >>, _: Ty<S< ^Y >>) : _
    when ^X: (static member eval: Ty< ^X > -> Ty< ^X' >)
     and ^Y: (static member eval: Ty< ^Y > -> Ty< ^Y' >)
     and (^X' or ^Y'): (static member gt: Ty< ^X' > * Ty< ^Y' > -> Ty< ^Z >) =
    ty< ^Z >

type GT<'x, 'y> = GT of 'x * 'y with
  static member inline eval (_: Ty<GT< ^X, ^Y>>) : _
    when ^X: (static member eval: Ty< ^X > -> Ty< ^X' >)
     and ^Y: (static member eval: Ty< ^Y > -> Ty< ^Y' >) =
    ((^X' or ^Y'): (static member gt: _*_ -> _) ty< ^X' >,ty< ^Y' >)

type LT<'x, 'y> = GT of 'x * 'y with
  static member inline eval (_: Ty<LT< ^X, ^Y>>) : _
    when ^X: (static member eval: Ty< ^X > -> Ty< ^X' >)
     and ^Y: (static member eval: Ty< ^Y > -> Ty< ^Y' >) =
    ((^X' or ^Y'): (static member gt: _*_ -> _) ty< ^Y' >,ty< ^X' >)

let y = eval ty<And<GT<Six, Three>, LT<Sub<Five, One>, Add<One, Three>>>>

y |> printfn "%A" // False

error FS0465: Type inference problem too complicated (maximum iteration depth reached). Consider adding further type annotations.