haskell-jp / questions #103 at 2023-04-27 15:41:54 +0900

GHC9.2.7を使っています。
type familyを用いて型レベル計算をしようとしており、他のtype familyの結果の型レベルタプルの複数要素の値を計算で使いたいです。
通常の関数であれば、タプルをletで束縛してからfstなりsndなりで結果を得られますが、type familyで同じようなことをするにはどうしたらよいですか？

具体的に、値レベルの場合let文を使えば下のコードのようにmydivmod一回の呼出しでタプルの両方の値を束縛して使えますが、同様のことををtype familyの定義中で行いたいです：

data MyNat = MyZero | MySucc MyNat deriving (Show, Eq)

mydivmod x y =
  case x of
    MyZero    -> (MyZero, MyZero)
    MySucc x' -> 
      let (d, m) = mydivmod x' y
      in  if (MySucc m) == y
          then (MySucc d, MyZero)
          else (d, MySucc m)

型レベルのバインディングは書けないので、以下のようにパターンごとに分けて定義することになります。再帰の場合は反復形（末尾再帰？）で定義するほうが定義しやすいと思います。

data Nat
    = Z
    | S Nat

type family (m :: Nat) + (n :: Nat) :: Nat where
    Z + n = n
    S m + n = S (m + n)

type family (m :: Nat) - (n :: Nat) :: Nat where
    Z - n = Z
    m - Z = m
    S m - S n = m - n

type family Cmp (m :: Nat) (n :: Nat) :: Ordering where
    Cmp Z     Z     = EQ
    Cmp Z     (S n) = LT
    Cmp (S m) Z     = GT
    Cmp (S m) (S n) = Cmp m n

type family DivMod (m :: Nat) (n :: Nat) :: (Nat, Nat) where
    DivMod m n = DivModIter Z (Cmp m n) m n

type family DivModIter (d :: Nat) (o :: Ordering) (m :: Nat) (n :: Nat) :: (Nat, Nat) where
    DivModIter d o   Z     (S b) = '(d  , Z)
    DivModIter d 'EQ (S a) (S b) = '(S d, Z)
    DivModIter d 'LT (S a) (S b) = '(d, S a)
    DivModIter d 'GT (S a) (S b) = DivModIter (S d) (Cmp (a - b) (S b)) (a - b) (S b)

type N2 = S (S Z)
type N5 = N2 + S N2

これで、たとえば

>>> :kind! DivMod N5 N2
DivMod N5 N2 :: (Nat, Nat)
= '( 'S ('S 'Z), 'S 'Z)

ですかね。