Dependent Types.md

依存型

• TBool ☑
• TInt
• TFloat
• TList

TBool.scala

package net.akouryy.lib.dtypes

import scala.language.{higherKinds, implicitConversions}
import scala.reflect.ClassTag

sealed trait TBool {
  type Not <: TBool
  type And[B <: TBool] <: TBool
  type Or [B <: TBool] <: TBool
  type If[X, Y]
}

class TTrue extends TBool {
  type Not = TFalse
  type And[B <: TBool] = B
  type Or [B <: TBool] = TTrue
  type If[X, Y] = X
}

class TFalse extends TBool {
  type Not = TTrue
  type And[B <: TBool] = TFalse
  type Or [B <: TBool] = B
  type If[X, Y] = Y
}

object TBool {
  type ![B <: TBool] = B#Not
  type &&[B1 <: TBool, B2 <: TBool] = B1#And[B2]
  type ||[B1 <: TBool, B2 <: TBool] = B1#Or[B2]
  type If[B <: TBool, X, Y] = B#If[X, Y]

  implicit def classTagOfNot[B <: TBool : ClassTag] =
    (if(value[B]) implicitly[ClassTag[TFalse]] else implicitly[ClassTag[TTrue]] ).asInstanceOf[ClassTag[![B]]]

  implicit def classTagOfAnd[B1 <: TBool : ClassTag, B2 <: TBool : ClassTag] =
    (if(value[B1]) implicitly[ClassTag[TTrue]] else implicitly[ClassTag[B2]]    ).asInstanceOf[ClassTag[B1 && B2]]

  implicit def classTagOfOr[B1 <: TBool : ClassTag, B2 <: TBool : ClassTag] =
    (if(value[B1]) implicitly[ClassTag[B2]]    else implicitly[ClassTag[TFalse]]).asInstanceOf[ClassTag[B1 || B2]]

  def value[B <: TBool : ClassTag]: Boolean = implicitly[ClassTag[B]].runtimeClass == classOf[TTrue]
}