部分的型付け

多相型推論をする言語を作りたいのですが、その前に部分的型付けを勉強しておきたい所です。TAPLのrcdsubbot*1から型付け部分だけ抜き出して名前をオレオレに変換してScalaで書いてみました。TopはScalaでいうとAny型で、どんな型でもTopの子になります。Botは最小型というどの型の子にでもなり得る、IPS細胞みたいな型です。サンプルコード*2の変数定義以外が動きます。

このプログラムで実現しているサブタイピングは構造的なサブタイピングといいます。C++等のオブジェクト指向の継承は、更に順番も必要になるでしょうが、サブタイピングの規則を書き換える事でいろいろなサブタイピングが出来るようになります。

package rcdsubbot

sealed trait T
case object TTop extends T // 最大の型
case object TBot extends T // 最小の型
case class TFun(t1: T, t2: T) extends T // 関数の型
case class TRecord(els: List[(String, T)]) extends T // レコードの型

sealed trait E
case class EVar(i: String) extends E // 変数
case class EFun(v: String, y: T, t: E) extends E // λ抽象
case class EApp(t1: E, t2: E) extends E // 関数適用
case class ERecord(fields: List[(String, E)]) extends E // レコード
case class EProj(t: E, proj: String) extends E // レコードのフィールド参照

object main extends App {
  // lambda x:Top.x
  println(typing(EFun("x",TTop,EVar("x"))))

  //((lambda x: Top -> Top. x) (lambda x: Top. x)): Top -> Top;
  println(typing(
    EApp(
      EFun("x",TFun(TTop,TTop),EVar("x")),
      EFun("x",TTop,EVar("x")))
  ))
  /*
  ((lambda r: {x: Top -> Top}. r.x (r.x))
      {x=lambda z: Top. z,
      y=lambda z: Top. z}):
    Top;
  */
  println(typing(
    EApp(
      EFun("r",TRecord(List("x"->TFun(TTop,TTop))),
        EApp(EProj(EVar("r"), "x"),EProj(EVar("r"), "x"))),
      ERecord(List(
        "x"->EFun("z",TTop,EVar("z")),
        "y"->EFun("z",TTop,EVar("z"))
      )))
  ))

  //(lambda x: Bot. x): Bot -> Bot;
  println(typing(EFun("x",TBot,EVar("x"))))


  //(lambda x: Bot. x x): Bot -> Bot;
  println(typing(EFun("x",TBot,EApp(EVar("x"),EVar("x")))))
}

object typing {

  def apply(e:E):T = {
    visit(Map(), e)
  }

  def subtype(cT:T, pT:T): Boolean = {
    cT == pT || // 
    ((cT, pT) match {
      case (_, TTop) => true // SA-Top
      case (TBot, _) => true // SA-Bot
      case (TFun(ct1,ct2), TFun(pt1,pt2)) => // SA-Arrow
        subtype(ct1, pt1) &&
        subtype(ct2, pt2)
      case (TRecord(css), TRecord(pts)) => // SA-Rcd
        pts.forall {
          case (s,pt) =>
            css.find{case (s1,_) => s1 == s} match {
              case Some((_,ct)) => subtype(ct, pt)
              case None => false
            }
        } 
      case _ => false
    })
  }

  def visit(env:Map[String,T], e:E):T = {
    e match {
    case EVar(v) => env(v) // TA-Var
    case EFun(v, t, e) => // TA-Abs
      val t2 = visit(env+(v->t), e)
      TFun(t, t2)
    case EApp(e1, e2) => // TA-App
      val t1 = visit(env, e1)
      val t2 = visit(env, e2)
      t1 match {
        case TFun(t11, t12) =>
          if (!subtype(t2, t11))
            throw new Exception("type error "+t2 + "!="+t12)
          t12
        case TBot => TBot // TA-AppBot
        case _ => throw new Exception("type error")
      }
    case ERecord(fs) => // TA-Rcd
      val fts = fs.map {
        case(s, e) => (s, visit(env, e))
      }
      TRecord(fts)
    case EProj(e1, s) => // TA-Proj
      visit(env, e1) match {
        case TRecord(fts) =>
          fts.find{case (s1, _) => s1 == s} match {
            case Some((_,t)) => t
            case None => throw new Exception("type error")
          }
        case TBot => TBot // TA-ProjBot
        case _ => throw new Exception("type error")
      }
    }
  }
}

*1:https://github.com/ilya-klyuchnikov/tapl-scala/tree/master/src/main/scala/tapl/rcdsubbot

*2:https://github.com/ilya-klyuchnikov/tapl-scala/blob/master/examples/rcdsubbot.tapl