11

のインスタンスであるデータ型を持っているMonoidので、素敵な値の構成を取得できます。

data R a = R String (Maybe (String → a))

instance Monoid (R a) where
  mempty = R "" Nothing
  R s f `mappend` R t g = R (s ++ t) (case g of Just _ → g; Nothing → f)

R a次に、すべての値を互いに結合したくありません。私のドメインでは意味がありません。だから私は幻のタイプを紹介しtます：

{-# LANGUAGE DataKinds, KindSignatures #-}

data K = T1 | T2
data R (t ∷ K) a = R String (Maybe (String → a))

instance Monoid (R t a) where …

だから私は「制限された」値を持っています:

v1 ∷ R T1 Int
v2 ∷ R T2 Int
-- v1 <> v2 => type error

および「無制限」:

v ∷ R t Int
-- v <> v1 => ok
-- v <> v2 => ok

しかし今、私には問題があります。v30たとえば、次のようになります。

  • 巨大なデータの種類を宣言します ( data K = T1 | … | T30)。タイプレベルのナチュラルを使用して、ファントムタイプの無限のソースを取得することで解決できます（治療は病気よりも悪いですよね？）
  • 依存コードで型シグネチャを記述するときに、どの値にどのファントム型を使用するかを覚えておく必要があります (これは本当に面倒です) 。

どういうわけか構成を制限する簡単な方法はありますか?

4

1 に答える 1

3

ConstrainedMonoidを探しています

最近、非常によく似た問題が発生しました。この問題は、この投稿の最後に記載されている方法で最終的に解決しました（モノイドではなく、型の述語を使用）。ConstrainedMonoidしかし、私は挑戦してクラスを書こうとしました。

アイデアは次のとおりです。

class ConstrainedMonoid m where
  type Compatible m (t1 :: k) (t2 :: k) :: Constraint
  type TAppend m (t1 :: k) (t2 :: k) :: k
  type TZero m :: k

  memptyC :: m (TZero m)
  mappendC :: (Compatible m t t') => m t -> m t' -> m (TAppend m t t')

ささいなインスタンスがありますが、実際には何も新しいものは追加されていません（Rs型引数を交換しました）：

data K = T0 | T1 | T2 | T3 | T4
data R a (t :: K) = R String (Maybe (String -> a))

instance ConstrainedMonoid (R a) where
  type Compatible (R a) T1 T1 = ()
  type Compatible (R a) T2 T2 = ()
  type Compatible (R a) T3 T3 = ()
  type Compatible (R a) T4 T4 = ()
  type Compatible (R a) T0 y = ()
  type Compatible (R a) x T0 = ()

  type TAppend (R a) T0 y = y 
  type TAppend (R a) x T0 = x
  type TAppend (R a) T1 T1 = T1
  type TAppend (R a) T2 T2 = T2
  type TAppend (R a) T3 T3 = T3
  type TAppend (R a) T4 T4 = T4
  type TZero (R a) = T0

  memptyC = R "" Nothing
  R s f `mappendC` R t g = R (s ++ t) (g `mplus` f)

残念ながら、これには多くの冗長な型インスタンスが必要です（OverlappingInstances型族では機能しないようです）が、型レベルでも値レベルでもモノイドの法則を満たしていると思います。

ただし、閉鎖されていません。これは、でインデックス付けされた一連の異なるモノイドのようなものKです。それがあなたが望むものなら、それで十分なはずです。

もっと欲しいなら

別のバリアントを見てみましょう。

data B (t :: K) = B String deriving Show

instance ConstrainedMonoid B where
  type Compatible B T1 T1 = ()
  type Compatible B T2 T2 = ()
  type Compatible B T3 T3 = ()
  type Compatible B T4 T4 = ()

  type TAppend B x y = T1
  type TZero B = T3 

  memptyC = B ""
  (B x) `mappendC` (B y) = B (x ++ y)

これはあなたのドメインで理にかなっているケースかもしれません-しかし、それはもはやモノイドではありません。そして、その1つを作成しようとすると、上記のインスタンスと同じになりますが、が異なりTZeroます。私は実際にはここで推測しているだけですが、私の直感では、有効なモノイドインスタンスはR a;のようなものだけであることがわかります。異なる単位値でのみ。

さもなければ、あなたは必ずしも連想的ではない何か（そしておそらくターミナルオブジェクトと）になってしまい、それは構成の下で閉じられません。また、構成をsに制限したい場合Kは、単位値が失われます。

より良い方法（IMHO）

これが私が実際に私の問題を解決した方法です（モノイドはとにかく意味をなさなかったので、当時はモノイドについてさえ考えていませんでした）。Compatibleこのソリューションは基本的に、2つのタイプの述語として残されている「制約プロデューサー」を除くすべてを取り除きます。

type family Matching (t1 :: K) (t2 :: K) :: Constraint
type instance Matching T1 T1 = ()
type instance Matching T2 T1 = ()
type instance Matching T1 T2 = ()
type instance Matching T4 T4 = ()

のように使用

foo :: (Matching a b) => B a -> B b -> B Int

これにより、互換性の定義、および必要な構成の種類（必ずしもモノイドではない）を完全に制御でき、より一般的です。無限の種類に拡張することもできます。

-- pseudo code, but you get what I mean
type instance NatMatching m n = (IsEven m, m > n)

最後の2つのポイントに答える：

  • はい、あなたはあなたの種類で十分に多くのタイプを定義する必要があります。しかし、とにかく彼らは自明であるべきだと思います。それらをグループに分割したり、再帰型を定義したりすることもできます。

  • 主に、制約の定義と、おそらくファクトリメソッド（）の2つの場所でインデックスタイプの意味を思い出す必要がありますmkB1 :: String -> B T1。しかし、タイプに適切な名前が付けられていれば、それは問題ではないと思います。（ただし、非常に冗長になる可能性があります。これを回避する方法はまだ見つかりません。おそらくTHが機能するでしょう。）

これはもっと簡単でしょうか？

私が実際に書きたいのは次のとおりです。

type family Matching (t1 :: K) (t2 :: K) :: Constraint
type instance Matching T1 y = ()
type instance Matching x T1 = ()
type instance Matching x y = (x ~ y)

これには許可されない重大な理由があるのではないかと思います。しかし、たぶん、それは実装されていないだけです...

編集：今日、私たちはまさにこれを行う閉じた型族を持っています。

于 2012-10-28T11:52:53.447 に答える