実行時にtrueであることがわかっている場合、タイプレベルの<=制約を満たすようにGHCに指示するにはどうすればよいですか?

Aug 17 2020

自然数でパラメーター化されたタイプがありますn

data MyType (n :: Nat) = MyType

このタイプの操作は、の場合n > 0にのみ意味があるため、制約として指定しました。

myFunction :: (KnownNat n, 1 <= n) => MyType n -> MyType n
myFunction = id

(注これらの関数の本当のバージョンがあることやるの使用をn持つ値にそれを回すことでnatVal。)

実行時にSomeMyType選択できる存在型()を作成したいと思いnます。

data SomeMyType where
  SomeMyType :: forall n. (KnownNat n, 1 <= n) => MyType n -> SomeMyType

の値を生成するためにSomeMyType、次のsomeMyTypeValように機能する関数を作成していますsomeNatVal

someMyTypeVal :: Integer -> Maybe SomeMyType
someMyTypeVal n
  | n > 0 = case someNatVal n of
      Just (SomeNat (_ :: p n)) -> Just (SomeMyType (MyType @n))
      Nothing                   -> Nothing
  | otherwise = Nothing

これは1 <= n制約がなくても完全に正常に機能しますが、制約があると次のタイプエラーが発生します。

• Couldn't match type ‘1 <=? n’ with ‘'True’
    arising from a use of ‘SomeMyType’

この制限を回避するにはどうすればよいですか?n > 0実行時に確認したので、このような操作を使用unsafeCoerceしてGHCに1 <= n真であると納得させてもかまいませんが、タイプレベルの値が失われるため、単に使用するunsafeCoerceことはできませんn

これに対処する最良の方法は何ですか?

回答

6 TikhonJelvis Aug 17 2020 at 05:21

もう少し調べてみると、同様の質問に対するJustinLの答えが見つかりました。彼は自分のソリューションをtypelits-witnessesパッケージにまとめました。このパッケージを使用して、この問題をかなりきれいに解決できました。

someMyTypeVal :: Integer -> Maybe SomeMyType
someMyTypeVal n = someNatVal n >>= check
  where check :: SomeNat -> Maybe SomeMyType
        check (SomeNat (_ :: p n)) = case (SNat @1) %<=? (SNat @n) of
          LE Refl -> Just (SomeMyType (MyType @n))
          NLE _ _ -> Nothing

a %<=? b2つのタイプレベルの自然数を比較して、abLE)より小さいかどうか(NLE)を確認できます。これにより、LEを返す場合に追加の制約が与えSomeMyTypeられますが、このNLE場合にそれを実行しようとすると、「「1 <=?n」と「True」を一致させることができません」というエラーが発生します。

の明示的な型シグネチャに注意してください。これがcheckないと、の型は次のようにcheck推測されcheck :: SomeNat -> Maybe a、次の型エラーが発生します。

• Couldn't match type ‘a’ with ‘SomeMyType’
   ‘a’ is untouchable
     inside the constraints: 'True ~ (1 <=? n)

明示的な型シグネチャを使用すると、すべてが機能し、コードは(合理的に)読み取り可能です。

1 K.A.Buhr Aug 19 2020 at 05:24

より直接的な答えとして、制約1 <= nはの型エイリアスにすぎません1 <=? n ~ 'True。次の方法で、このような型の等式制約を安全に作成できません。

{-# LANGUAGE DataKinds, TypeOperators #-}

import Data.Type.Equality
import GHC.TypeLits
import Unsafe.Coerce

unsafeDeclarePositive :: p n -> (1 <=? n) :~: 'True
unsafeDeclarePositive _ = unsafeCoerce Refl

これは多かれ少なかれ内部typelits-witnessesで行っていることです。

その定義が整ったら、次のようにタイプチェックする必要があります。

someMyTypeVal :: Integer -> Maybe SomeMyType
someMyTypeVal n
  | n > 0 = case someNatVal n of
      Just (SomeNat (pxy :: p n)) ->
        case unsafeDeclarePositive pxy of
          Refl -> Just (SomeMyType (MyType @n))
      Nothing -> Nothing
  | otherwise = Nothing