11

データの種類、型ファミリ、および type-nats を使用するようにllvmパッケージの移植にゆっくりと取り組んできましたが、値の分類に使用される 2 つの新しい型(ConstValueおよび) を削除しようとすると、小さな問題が発生しました。一貫性。ValueValue

CallArgs引数のみを受け入れ、 aを aValue 'Variable aにキャストする関数を提供します。各引数が または のいずれかになるように一般化したいと思います。タイプファミリを使用してこれを何らかの方法でエンコードすることは可能ですか? おそらくファンデプスで可能だと思います。Value 'Const aValue 'Variable aCallArgs'Const'Variable

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}

data Const = Const | Variable

data Value (c :: Const) (a :: *)

type family CallArgs a :: * 
type instance CallArgs (a -> b) = forall (c :: Const) . Value c a -> CallArgs b
type instance CallArgs (IO a)   = IO (Value 'Variable a)

...コンパイルに失敗します：

/tmp/blah.hs:10:1:
    不正なポリモーフィックまたは修飾型:
      forall (c :: Const)。値 ca
    「CallArgs」の型インスタンス宣言で

次の解決策は機能しますが (従来のコードと同等)、ユーザーが each 定数をキャストする必要がありますValue。

type family CallArgs' a :: * 
type instance CallArgs' (a -> b) = Value 'Variable a -> CallArgs' b
type instance CallArgs' (IO a)   = IO (Value 'Variable a)
4

2 に答える 2

6

CallArgsあなたが求めているのは、またはのいずれかを受け取って返す非決定論的関数のようなものa -> bです。非決定論的関数で時々できることの1つは、それらを裏返すことです。確かに、これには決定論的な逆関数があります。Value 'Const a -> blahValue 'Variable a -> blah

type family   UnCallArgs a
type instance UnCallArgs (Value c a -> b) = a -> UnCallArgs b
type instance UnCallArgs (IO 'Variable a) = IO a

さて、あなたが次のようなタイプを書いたであろうところならどこでも

foo :: CallArgs t -> LLVM t

またはそのようなもの、代わりにこれを書くことができます：

foo :: t -> LLVM (UnCallArgs t)

もちろん、それよりも良い名前を選ぶこともできますがUnCallArgs、Nativeそれをうまく行うには、私が持っていないドメイン知識が少し必要です。

于 2012-12-12T20:23:31.880 に答える
3

forall c をラッピングします。あなたのためのnewtype AV仕事で？

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}

data CV = Const | Variable

data Value (c :: CV) (a :: *)

data AV a = AV (forall c. Value c a)

type family CallArgs a :: * 
type instance CallArgs (a -> b) = AV a -> CallArgs b
type instance CallArgs (IO a)   = IO (Value 'Variable a)
于 2012-12-12T21:06:59.180 に答える