型レベルズンドコキヨシ 2 #Scala

@ryoppy さんに先を越されてしまったが、こちらはマクロじゃなくて線形合同法でやってみます。

定式化

オリジナルのズンドコキヨシは

「ズン」「ドコ」のいずれかをランダムで出力し続けて「ズン」「ズン」「ズン」「ズン」「ドコ」の配列が出たら「キ・ヨ・シ！」って出力した後終了って関数作ったら満点で単位貰ってた

ですが、今回は型レベルで実装したいので、もう少し問題を定式化する必要があります。

ここでは、以下をズンドコキヨシと定義して解くことにします。

定数A, C, Mおよび初期値$X_0$, 閾値Tを与え、次の式でズンドコ列{$Zn$}を生成する (線形合同法)
- $X_{n+1} = (AX_n+C)modM$ に対し、$Xn >= T$ならズン, $Xn < T$ならドコ
$Z_{n-3}, Z_{n-2}, Z_{n-1}, Z_{n}$ = ズン, ズン, ズン, ドコをみたす$n$が見つかったら、{$Z_n$}の後にキ・ヨ・シ！を出力して終了

線形合同法でズン or ドコを出力

import shapeless._, nat.ops._

trait ズン
trait ドコ
trait `キ・ヨ・シ！`
case object ズン extends ズン
case object ドコ extends ドコ
case object `キ・ヨ・シ！` extends `キ・ヨ・シ！`

trait GenZD[A <: Nat, C <: Nat, M <: Nat, X <: Nat, T <: Nat, ズンドコ, OutX <: Nat] {
  def apply: ズンドコ
}

object GenZD {
  implicit def zun[A <: Nat, C <: Nat, M <: Nat, X <: Nat, T <: Nat, `A*X` <: Nat, `A*X+C` <: Nat, `(A*X+C)%M` <: Nat](
    implicit prod: Prod.Aux[A, X, `A*X`], sum: Sum.Aux[`A*X`, C, `A*X+C`], mod: Mod.Aux[`A*X+C`, M, `(A*X+C)%M`], gteq: GTEq[`(A*X+C)%M`, T]): GenZD[A, C, M, X, T, ズン, mod.Out] =
    new GenZD[A, C, M, X, T, ズン, mod.Out] {
      def apply: ズン = ズン
    }

  implicit def doko[A <: Nat, C <: Nat, M <: Nat, X <: Nat, T <: Nat, `A*X` <: Nat, `A*X+C` <: Nat, `(A*X+C)%M` <: Nat](
    implicit prod: Prod.Aux[A, X, `A*X`], sum: Sum.Aux[`A*X`, C, `A*X+C`], mod: Mod.Aux[`A*X+C`, M, `(A*X+C)%M`], lt: LT[`(A*X+C)%M`, T]): GenZD[A, C, M, X, T, ドコ, mod.Out] =
    new GenZD[A, C, M, X, T, ドコ, mod.Out] {
      def apply: ドコ = ドコ
    }
}

テストしてみます

implicitly[GenZD[_3, _2, _4, _1, _2, ドコ, _1]].apply // (3 * 1 + 2) % 4 = 1は2より小さくドコなのでOK
implicitly[GenZD[_3, _2, _4, _1, _2, ズン, _1]].apply // コンパイルできない

ズンドコキヨシ

ズンドコを得る関数ができたので、ズンドコキヨシを実装していきます。

trait ZDK[A <: Nat, C <: Nat, M <: Nat, X <: Nat, T <: Nat, Acc <: HList] {
  type Out <: HList
  def apply(acc: Acc): Out
}

trait LowerPriorityZDK {

  implicit def loop[A <: Nat, C <: Nat, M <: Nat, X <: Nat, T <: Nat, ZD, NextX <: Nat, Acc <: HList](
    implicit genZD: GenZD[A, C, M, X, T, ZD, NextX], zdk: Lazy[ZDK[A, C, M, NextX, T, ZD :: Acc]]): ZDK[A, C, M, X, T, Acc] =
    new ZDK[A, C, M, X, T, Acc] {
      type Out = zdk.value.Out
      def apply(acc: Acc): Out = zdk.value(genZD.apply :: acc)
    }
}

object ZDK extends LowerPriorityZDK {
  type Aux[A <: Nat, C <: Nat, M <: Nat, X <: Nat, T <: Nat, Acc <: HList, Out0 <: HList] = ZDK[A, C, M, X, T, Acc] { type Out = Out0 }

  implicit def end[A <: Nat, C <: Nat, M <: Nat, X <: Nat, T <: Nat, Acc <: HList](
    implicit ev: Acc <:< (ドコ :: ズン :: ズン :: ズン :: HList)): ZDK[A, C, M, X, T, Acc] = new ZDK[A, C, M, X, T, Acc] {

    type Out = `キ・ヨ・シ！` :: Acc
    def apply(acc: Acc): Out = `キ・ヨ・シ！` :: acc
  }

  def apply[A <: Nat, C <: Nat, M <: Nat, Init <: Nat, T <: Nat, Acc <: HList](implicit zdk: ZDK[A, C, M, Init, T, Acc]): Aux[A, C, M, Init, T, Acc, zdk.Out] = zdk
}

試してみます。
$A=5, C=3, M=8, X_0=1, T=4$で上記の方法で乱数列$X_1, X_2,...$とズンドコ列$Z_1, Z_2,...$を生成すると

$X_1,X_2,... = 0, 3, 2, 5, 4, 7, 6, 1, 0, ...$
$Z_1,Z_2,... = ドコ, ドコ, ドコ, ズン, ズン, ズン, ズン, ドコ, ドコ, ...$

なので、 キ・ヨ・シ！ :: ドコ :: ズン :: ズン :: ズン :: ズン :: ドコ :: ドコ :: ドコ :: HNil となるはずです。

scala> implicitly[ZDK[_5, _3, _8, _1, _4, HNil]].apply(HNil)
res1: ZDK[shapeless.Nat._5,shapeless.Nat._3,shapeless.Nat._8,shapeless.Nat._1,shapeless.Nat._4,shapeless.HNil]#Out = キ・ヨ・シ！ :: ドコ :: ズン :: ズン :: ズン :: ズン :: ドコ :: ドコ :: ドコ :: HNil

できたー！！

けど、

REPLに貼っつけるとうまくいく(コンパイルにかなり時間かかるが)
implicitly[ZDK[_5, _3, _8, _1, _4, HNil]].apply(HNil)を一緒のソースに入れてコンパイルするとcompile error

mkLazyマクロの影響と思うが...

型レベルズンドコキヨシ 2

定式化

線形合同法で ズン or ドコを出力

ズンドコキヨシ

参考

線形合同法でズン or ドコを出力