2

I use vinyl to declare a number of different record types, some of which have a field called Content with a specific type LanguageContent. For the functions that depend on the field being present in the record, I want to have a type like:

getContent :: HasContent a => a -> LanguageContent
getContent a = a ^. rlens SContent . unAttr

(Function given for illustration only; there are many functions taking something that HasContent and doing different things with it.)

Now I just need to declare HasContent as a constraint. The closest I can get using Data.Vinyl.Notation is:

getContent :: (Content ∈ fs) => Rec Attr fs -> LanguageContent

A type family can be declared but the function does not typecheck:

type family HasContent c :: Constraint
type instance HasContent (Rec Attr rs) = Content ∈ rs

getContent :: HasContent a => a -> LanguageContent
getContent a = a ^. rlens SContent . unAttr

Could not deduce (a ~ Rec Attr rs0)
from the context (HasContent a)

I can make a constraint with two parameters which works but isn't ideal (rs is a parameter that I have to repeat everywhere):

type HasContent c rs = (c ~ Rec Attr rs, Content ∈ rs)

Without the extra parameter (see answer by @ChristianConkle), I just get:

type HasContent c = (c ~ Rec Attr rs, Content ∈ rs)

Not in scope: type variable ‘rs’

How do I declare a constraint which only holds for such Rec Attr fs that Content ∈ fs?

Koterpillar
  • 7,883
  • 2
  • 25
  • 41
  • 1
    What is wrong with the inferred type - which is precisely `Content ∈ fs => Rec Attr fs -> LanguageContent`? This type is much more descriptive than `HasContent a => a -> LanguageContent`. If you really want the latter, define a class `class HasContent a where getContent :: a -> LanguageContent` and an instance `instance (Content ∈ rs) => HasContent (Rec Attr rs) where ...`. If you plan to have other instances, this approach has merit, but if this is the only instance, just use the function as-is. – user2407038 Mar 04 '15 at 22:19
  • There are quite a few functions which all have the same constraint, and I don't want to repeat it everywhere. – Koterpillar Mar 04 '15 at 23:41
  • It's not strictly proper to integrate answers into the question. If you want to include bits from the answers @user2407038 and I provided, please explain what you're doing in the answer so that the conversation doesn't become confusing. – Christian Conkle Mar 09 '15 at 00:10
  • Also, referring to `rs` in the type `(c ~ Rec Attr rs, Content ∈ rs)` as a "phantom parameter" is unhelpful. In fully monomorphic code, `rs` will be specialized to a specific, concrete, meaningful value representing the fields or rows of the record. – Christian Conkle Mar 09 '15 at 00:23

1 Answers1

2

Edit: @Koterpillar's test file seems to demonstrate that this type synonym doesn't work the way I expected; it appears the constraint is not available inside the definition. It'd be worth investigation or a follow-up question to determine why. It had been my understanding that (C x => T x) -> Y was equivalent to C x => T x -> Y, but the fact that the example doesn't work seems to belie that. /Edit

I think you want to write this instead:

type RecWithContent rs = Content ∈ rs => Rec Attrs rs

getContent' :: RecWithContent rs -> LanguageContent

This is really just wrapping up the constraint in a type synonym. You need RankNTypes and probably a bunch of other extensions.

Your existing attempts to solve the problem and leave just a on the right hand side of the => boil down to this type synonym:

type HasContent c = (Content ∈ fs, c ~ Rec Attr fs)

In other words, you want HasContent to witness two separate things: that Content is in fs, and that the type parameter c is equal to Rec Attr fs.

I don't think you can do this in a way that's convenient for you. With the type synonym, the surface-level problem is that rs is not in scope on the right hand side. The deeper issue is that you're asking the compiler to make up fs; you want to write something like exists fs. (Content ∈ fs, c ~ Rec Attr fs), which is not expressible directly in current Haskell.

Your type family solution won't help, but for a different reason. In the definition of getContent, the compiler needs proof that a really is Rec Attr rs0 in order to use rlens (or probably unAttr), but it can't deduce that from the type family. (You know that there's only one type instance, but the compiler doesn't use that logic.)

Christian Conkle
  • 5,932
  • 1
  • 28
  • 52
  • What are `b` and `a` in the definitions of `RecWithContent`? With or without them, I get this: http://lpaste.net/121586 – Koterpillar Mar 05 '15 at 10:25
  • Sorry, I messed up the type variables; I shouldn't have included `b` or `a`; I've edited the answer. The definition in your lpaste, `type HasContent = (Content ∈ rs) => Rec Attr fs`, won't work because the `rs` is hidden on the right-hand side of the type synonym; it needs to be exposed in the signature of the overall function to eliminate the ambiguity. – Christian Conkle Mar 05 '15 at 19:49
  • To fix the first error, fix the typo in the definition of `HasContent`. There's only one type variable. The second error might be something else; your `unAttr` may be too polymorphic to fix `fs0` and `i0`. Does your original `getContent :: Content ∈ fs => Rec Attr fs -> LanguageContent` typecheck? The signatures should be equivalent, unless I'm mistaken. – Christian Conkle Mar 06 '15 at 19:07
  • http://lpaste.net/123101. `getContent` with the constraint specified manually typechecks, as well as the two-parameter typeclass (`HasContent a rs`, as in the question). – Koterpillar Mar 06 '15 at 22:16
  • I don't think there's enough information in [123101](http://lpaste.net/123101) and your comment to explain the error. Please include a [minimum, complete, verifiable example](http://stackoverflow.com/help/mcve) in the question. – Christian Conkle Mar 09 '15 at 00:20
  • Hmm. Sorry, then; it looks like my "best" solution doesn't work. There must be something I'm misunderstanding about the way GHC deals with nested constraints. (It's not a well-specified corner of the language.) You could ask a follow-up question if you're interested in that approach. – Christian Conkle Mar 13 '15 at 16:10