2

私はData.Typeable.gcast、ある種の型族で機能するバリアントを書き込もうとしてい* -> *ます。私が探しているのは：

{-# LANGUAGE TypeFamilies #-}
import Data.Typeable

type family T

gcastT :: (Typeable a,Typeable b) => T a -> Maybe (T b)
gcastT = undefined -- but that's not working too well!

に類推して行きgcast :: (Typeable a,Typeable b) => f a -> Maybe (f b)ます。

これは可能ですか？

コンテキストをに変更することもでき(Typeable (T a),Typeable (T b)) =>ますが、美的理由からこの署名を使用したいと思います。結局のところ、gcast必要ありません。Typeable1 f

私が実際に達成したいことについて間違った問題を解決している場合の背景：私の目標は関数を書くことですmatchAndExtract：

matchAndExtract :: (Eq a, Typeable a, Eq b, Typeable b) => a -> b -> T b -> Maybe (T a)
matchAndExtract x k v = if (cast x == Just k) then gcastT v else Nothing

これは、同じタイプであり、等しいかどうかをチェックxし、提供されたものを返します（これは、それまでに-Tと同じであることがわかっていますが、単射ではないかもしれませんが、関数です！）または、それ以外の場合。kT bT aNothing

T a問題のあるものをでラップしnewtype、を使用してgcast、再度ラップを解除することで回避策があります。

matchAndExtractF :: (Eq a, Typeable a, Eq b, Typeable b) => a -> b -> f b -> Maybe (f a)
matchAndExtractF x k v = if (cast x == Just k) then gcast v else Nothing

newtype WrapT a = WrapT { unWrapT :: T a }

matchAndExtractViaWrap :: (Eq a, Typeable a, Eq b, Typeable b) => a -> b -> T b -> Maybe (T a)
matchAndExtractViaWrap x k v = fmap unWrapT $ matchAndExtractF a k (WrapT v)

しかし、それは私を間違った方法でこすります！これは、 ;T aのインスタンスではないインスタンスでも機能します。これもまた、コンテキストが必要ではないことTypeableを示しているように思えます。Typeable (T a)

WrapT回避策は完全に受け入れられますが、スプリアスタイプを取り除きたいと思います。

4

1 に答える 1

3

あなたがやろうとしていることは、あなたがそれを実装した方法では不可能です。代わりに使用できます

type family T x :: *
newtype NT x = NT {fromNT :: T x}
gcastT :: (Typeable a, Typeable b) => NT a -> Maybe (NT b)
gcastT = gcast

この場合、Eq制約を使用する必要はありません。

別のオプションは、入力可能な辞書をGADTに具体化することです。

data Type x where
  Typeable :: Typeable x => Type x

asT :: NT x -> Type x -> NT x
asT = const

gcastTD :: Type a -> Type b -> Type a -> Maybe (T b)
gcastTD t@Typeable Typeable x = fmap fromNT $ gcastT $ (NT x) `asT` t

（コードはテストされていませんが、ほぼ正しいはずです）

これを取得したら、明示的な型シグネチャを渡すことで使用できます

type instance T Int = ()

justUnit = gcastTD (Typeable :: Type Int) (Typeable :: Type Int) ()
于 2013-02-28T21:45:30.380 に答える