実行時にtrueであることがわかっている場合、タイプレベルの<=制約を満たすようにGHCに指示するにはどうすればよいですか?
自然数でパラメーター化されたタイプがあります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
。
これに対処する最良の方法は何ですか?
回答
もう少し調べてみると、同様の質問に対する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 %<=? b
2つのタイプレベルの自然数を比較して、a
がb
(LE
)より小さいかどうか(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 <= 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