プロモーションタイプNat = Suc Nat | Zero
とタイプメッシュclass C (a :: Nat) b
を作りたいと思います。 GHCにinstance C Zero b
とinstance C (Seq x) b
がすべてのケースをカバーしていると確信させる方法はありますか?したがって、クラスのメソッドを使用するときはいつも、C
を制約として明示的に宣言する必要はありません。ここではいくつかのコードは次のとおりです。プロモーションタイプの型抜きチェック
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE IncoherentInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
-- Some of these may not be necessary for the particular snippet.
data Nat = Zero | Suc Nat
-- TypeApplications, I know. I am traditional.
data NProxy :: Nat -> * where
NProxy :: NProxy n
class C (a :: Nat) b where
f :: NProxy a -> b -> Maybe b
instance C Zero b where
f _ _ = Nothing
instance C (Suc a) b where
f _ = Just
-- instance C n b where
-- f = error "This should not have been reached using GetNum."
class C1 a where
f1 :: a -> Maybe a
instance C1 a where
f1 = Just
type family GetNum a :: Nat where
GetNum Char = (Suc Zero)
GetNum Int = Suc (Suc Zero)
GetNum [x] = Suc (GetNum x)
GetNum a = Suc Zero
-- Error:
-- • No instance for (C (GetNum a) a) arising from a use of ‘f’
-- • In the expression: f (NProxy :: NProxy (GetNum a)) x
-- In an equation for ‘noGreet’:
-- noGreet x = f (NProxy :: NProxy (GetNum a)) x
noGreet :: forall a . a -> Maybe a
noGreet x = f (NProxy :: NProxy (GetNum a)) x
-- This one works fine though.
dumb :: a -> Maybe a
dumb = f1
編集:関連する質問は、私は例外を取得していないJust "hi"
REPLにnoGreet "hi"
を言うとき、それをある理由をコメントアウトインスタンスC
場合、与えられた、だろう。 Parametricityが、このタイプの唯一の定義可能な値は「a
がChar
そうJust x
であればNothing
」私たちは次のように、タイプa
に依存するすべての選択を行うことができない
noGreet x = Just x
noGreet x = Nothing
noGreet x = undefined
noGreet x = x `seq` Just x
...
のようなものですと言う
いいえ、すべての型にスタック型のファミリーが存在するため、 '' Nat''が偽である '' Z''と '' Sn''だけで '' Nat' Any :: Nat'と 'Any Any :: Nat'、無限の宣言。さらに、明示的な制約の必要性はなくなりません。制約は、実際にタイプレベルの計算を実行できるようにすることです。 'dumb'は、あなたがその型に何の制約も課されない、すべての型' a'に対してインスタンス 'C1 a'を持っているので動作します。 – user2407038
私はあなたの答えに感謝します。 IncoherentInstancesを使って型システムを欺く方法はありますか(edit参照)? – fakedrake
'noGreet'に型エラーがあるので例外が発生します。したがって、' noGreet anything'も常に型エラーになります。 'IncoherentInstances'は明確に定義されたセマンティクスを持っていないので、これまでどんな助けにもならないはずです。 – user2407038