Haskellで依存型を多相的に扱うのはやめた方がよいらしい

バイトでHaskellを書いている．
その中で，表現は共通だが2つの形式を持っているデータを型で区別したいということがあったので，幽霊型でいいじゃん！と思いDataKindsを使って実装しPRを出したところ，Haskellの強い方から「Haskellで依存型を多相的に扱うのはやめたほうがよい」と指摘して頂いたので実際どう駄目なのかをコードを書いて見てみた．

とりあえず依存型ということで型レベル自然数を使った長さ付きリストと安全なheadを実装してみる．

import GHC.TypeNats

data IxList l a where
  Nil :: IxList 0 a
  Cons :: a -> IxList l a -> IxList (succ l) a

safeHead :: (1 <= n) => IxList n a -> a
safeHead (Cons x _) = x

safeHaedのConstraintで1 <= n，すなわちリストの長さが1以上であることを要求しており，Nilに対して適用されないことが保証されるので，-Wallを付けてコンパイルしても警告がでない．

ここで同様に安全なtailを定義してみる．

safeTail :: (1 <= n) => IxList n a -> IxList (pred n) a
safeTail (Cons _ xs) = xs

しかしこれは以下のエラーでコンパイルに失敗する．

[-Wdeferred-type-errors]
    * Occurs check: cannot construct the infinite type:
        l ~ pred (succ l)
      Expected type: IxList (pred n) a
        Actual type: IxList l a
    * In the expression: xs
      In an equation for `safeTail': safeTail (Cons _ xs) = xs
    * Relevant bindings include
        xs :: IxList l a
          (bound at /home/haneta/temp/dependent-type/.stack-work/intero/interoEbUeve-TEMP.hs:17:18)
        safeTail :: IxList n a -> IxList (pred n) a
          (bound at /home/haneta/temp/dependent-type/.stack-work/intero/interoEbUeve-TEMP.hs:17:1)

(~)は* -> * -> Constraintのカインドを持っていて左右の型が等しいという制約を意味する型演算子である． つまりGHCの能力ではl ~ pred (succ l)が等しいということが分からず，型検査に失敗してしまう．

これは人間にはもちろん等しいということが分かるし，依存型をきちんと扱える処理系でもきちんと検査できる．

たとえばAgdaでは以下のコードは型検査が通る．

module IxList where

open import Data.Nat

data IxList (A : Set) : ℕ → Set where
  nil : {n : ℕ} → IxList A 0
  cons : {n : ℕ} → A → IxList A n → IxList A (suc n)

safeHead : {A : Set} → {l : ℕ} → (0 < l) → IxList A l → A
safeHead () nil
safeHead  _ (cons x _) = x

safeTail : {A : Set} → {l : ℕ} → (0 < l) → IxList A l → IxList A (pred l)
safeTail () nil
safeTail _ (cons _ xs) = xs

現状のHaskellは依存型を実用するにはまだ早いが，依存型をHaskellで扱えるようにするDependent Haskellというプロジェクトがあるようで将来的には依存型をバリバリ使ったプログラミングができるのかもしれない．