Note that there are some explanatory texts on larger screens.

plurals
  1. PO
    primarykey
    data
    text
    <p><strong>Looking for the ConstrainedMonoid</strong></p> <p>I came to a very similar problem lately, which I finally solved the way described at the end of this post (not involving a monoid, but using predicates on types). However, I took the challenge and tried to write a <code>ConstrainedMonoid</code> class.</p> <p>Here's the idea:</p> <pre><code>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') =&gt; m t -&gt; m t' -&gt; m (TAppend m t t') </code></pre> <p>Ok, there's the trivial instance, which in fact doesn't add anything new (I swapped <code>R</code>s type arguments):</p> <pre><code>data K = T0 | T1 | T2 | T3 | T4 data R a (t :: K) = R String (Maybe (String -&gt; 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) </code></pre> <p>This unfortunately takes a lot of redundant type instances (<code>OverlappingInstances</code> don't seem to work for type families), but I think it satisfies the monoid laws, at type level as well as at value level. </p> <p>However, it is not closed. It's more like a set of different monoids, indexed by <code>K</code>. If that's what you want, it should suffice.</p> <p><strong>If you want more</strong></p> <p>Let's look at a different variant:</p> <pre><code>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) </code></pre> <p>This could be a case which makes sense in your domain -- however, it is not a monoid anymore. And if you tried to make one of it, it'll get the same as the instance above, just with different <code>TZero</code>. I'm actually just speculating here, but my intuition tells me that the only valid monoid instances are exactly the ones like for <code>R a</code>; only with different unit values.</p> <p>Otherwise, you'll end up with something not neccessarily associative (and probably with a terminal object, I think), which is <em>not</em> closed under composition. And if you want to restrict composition to equal <code>K</code>s, you'll lose the unit value.</p> <p><strong>A better way (IMHO)</strong></p> <p>Here's how I actually solved my problem (I didn't even think of monoids back then, since they didn't make sense anyhow). The solution essentially strips off everything except the <code>Compatible</code> "constraint producer", which is left as a predicate on two types:</p> <pre><code>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 = () </code></pre> <p>used like</p> <pre><code>foo :: (Matching a b) =&gt; B a -&gt; B b -&gt; B Int </code></pre> <p>This gives you full control over your definition of compatibility, and what kind of composition (not necessarily monoidal) you want, and it is more general. It can be expanded to infinite kinds, too:</p> <pre><code>-- pseudo code, but you get what I mean type instance NatMatching m n = (IsEven m, m &gt; n) </code></pre> <hr> <p>Answering your two last points: </p> <ul> <li><p>Yes, you have to define sufficiently many types in your kind. But I think that they should be self-explaining anyway. You could also split up them into groups, or define a recursive type.</p></li> <li><p>You mainly have to remind the meaning of the index type at two places: the definition of the constraint, and maybe for factory methods (<code>mkB1 :: String -&gt; B T1</code>). But I think that shouldn't be the problem, if the types are named well. (It <em>can</em> be very redundant, though -- I've not found a way to avoid that yet. Probably TH would work.)</p></li> </ul> <p><strong>Could this be easier?</strong></p> <p>What I'd actually like to be able to write is the following:</p> <pre><code>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) </code></pre> <p>I fear this has a serious reason not to be allowed; however, maybe, it's just not implemented... </p> <p><strong>EDIT:</strong> Nowadays, we have <a href="http://www.haskell.org/haskellwiki/GHC/Type_families#Detailed_definition_of_type_synonym_families" rel="nofollow">closed type families</a>, which do exactly this.</p>
    singulars
    1. This table or related slice is empty.
    plurals
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. VO
      singulars
      1. This table or related slice is empty.
    2. VO
      singulars
      1. This table or related slice is empty.
    3. VO
      singulars
      1. This table or related slice is empty.
 

Querying!

 
Guidance

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload