4

I think I get it with the "unusual form" of constraints. Just checking ...

The examples in that section for Provided constraints (the second one) all seem to involve GADTs/existentials inside the data constructor(?) With the answer here, I'm not sure if an existential is involved (in the Vinyl library), but the type for rhead has a more specific type than the argument that f is passing to it. And tbh the PatternSynonym seems to be a red herring: the arguments to OnlyRecord don't appear on f's rhs.

Required constraints (the first one of two, or the only one if there's one) seem to give the same functionality as the now-deprecated DatatypeContexts(?) For example

data NoCSet a  where                      -- no constraints on the datatype
  NilSet_  :: NoCSet a
  ConsSet_ :: a -> NoCSet a -> NoCSet a
         deriving (Eq, Show, Read)

pattern ConsSet :: (Eq a) => ()     => a -> NoCSet a -> NoCSet a
                -- Req'd  => Prov'd => type;         Prov'd is empty, so omittable
pattern ConsSet x xs = ConsSet_ x xs

pattern NilSet :: (Eq a) => () => NoCSet a
pattern NilSet  = NilSet_

ccUnit = ConsSet () NilSet                     -- accepted
-- ccid   = ConsSet id NilSet                  -- rejected no instance Eq (a -> a)
-- ncid   = NilSet :: NoCSet (a -> a)          --   ditto

with the extra advantage I can put a Required constraint on a pattern NilSet without an argument, disallowing building even an empty set with an unacceptable type. DatatypeContexts for constructors like that just ignore the constraint.

Edit/focussed question: (response to @Noughtmare comment)

Is there an observable difference between pattern ConsSet defined above vs constructor DCConsSet here:

data (Eq a) => DCSet a  =          -- constraint on the datatype
    DCNilSet
  | DCConsSet a (DCSet a)
         deriving (Eq, Show, Read)

I mean "difference" other than one's a pattern, one's a constructor. I've tried using them in both building and matching values; I get same behaviour.

AntC
  • 2,623
  • 1
  • 13
  • 20
  • Can you formulate a clear focused question? Now it seems to me like you are broadly asking if the things you are writing are correct. – Noughtmare Jun 14 '21 at 10:33
  • If you're asking specifically about `DatatypeContexts` because you want to use it, I doubt that this direction would be fruitful. If you want a type which structurally resembles `NoCSet` but also "disallowing building even an empty set with an unacceptable type" then how about `data CSet a where CSet :: Eq a => NoCSet a -> CSet a`? – user2407038 Jun 14 '21 at 15:27
  • @user2407038, no a GADT/existential constraint is a Provided -- that's a different type. I want to prevent building a `Set` unless `Eq a`. (And I wasn't trying to debate `DatatypeContexts` -- SO isn't the place for debates; I'm familiar with the arguments.) – AntC Jun 14 '21 at 21:15
  • @AntC GADT constraint is both required and provided. You can simply ignore the provided constraint if you don't want to use it. It seems to me this would accomplish the goal of "disallowing building even an empty set with an unacceptable type". It also accomplishes a different thing, namely to prove `CSet a -> (Eq a => r) -> r`. Or is the idea specifically to require an `Eq` constraint but then to forget it once its been provided? – user2407038 Jun 14 '21 at 21:42
  • Inferred types: `(\(ConsSet x xs) -> x) :: Eq a => NoCSet a -> a`; `(\(DCConsSet x xs) -> x) :: Eq a => DCSet a -> a`; `(\(CSet (ConsSet_ x xs)) -> x) :: CSet p -> p`; `(\(GADTConsSet x xs) -> x) :: GADTSet p -> p`. Observably different types. The GADT Provided constraint is visible only inside the pattern match. Your embedded `(Eq a => r)` needs `RankNTypes` and even then `GHC doesn't yet support impredicative polymorphism` (at 8.10.2). – AntC Jun 15 '21 at 01:15
  • @AntC You're certainly correct about the types of those terms. I think I just don't understand your goal here. Surely this type for `(\(ConsSet x xs) -> x)` is not useful, as any value constructed with `ConsSet` already requires `Eq` and you require the constraint again when you match on `ConsSet` (even though you already "know" the constraint must be true). It seems you have answered your question already ("Is there an observable difference...") – user2407038 Jun 15 '21 at 15:49

1 Answers1

0

No, in general, required constraints don't simply give the same functionality as data type contexts. Data type contexts introduce a constraint that is required to either construct or destruct the value for no reason other than the programmer who created the data type wants to force users of that data type to satisfy that constraint. They are deprecated because it's now considered bad practice to require a constraint for an operation (data type construction or destruction) that does not need the constraint. Instead, the constraints should be moved closer to the "usage site". When the data type is used in a manner that requires a constraint, that's where the constraint should appear. (It sounds like you're familiar with this reasoning.)

In contrast, when used correctly, required constraints on patterns introduce a constraint that is required to construct or destruct the value because the construction or destruction of that value makes use of the provided instance.

For example, given:

{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE PatternSynonyms #-}

pattern Length n <- (length -> n)

the inferred type of Length is:

pattern Length :: Foldable t => Int -> t a

Here, Foldable t is a required constraint here because it is actually needed when matching the pattern.

As you note, you can misuse patterns with required constraints to mimic the deprecated data type contexts extension, but while you're technically not using the deprecated extension, you're still doing something that's widely considered bad practice.

As for your final question, data types with context and patterns with required constraints are handled rather differently by the compiler, so there are bound to be diffferences. One observable difference is that with DataKinds enabled, DCNilSet is a type, while NilSet isn't.

If your real question is "does the existence of required constraints on patterns represent an admission on the part of the Haskell community that data type contexts are actually a valuable feature that should have never been deprecated?", I think the answer is probably "no".

K. A. Buhr
  • 45,621
  • 3
  • 45
  • 71
  • Thanks for the long answer, it'll need some thinking about. Re your last para: DT contexts 1991 design was always a misfeature/stupid theta. I'm wondering (sorry to be vague) if PatternSyn Required constraints are a) closer to the original 1990 design; b) better because you can put the Req'd constraint on `Nilset` even though it doesn't have an `a` argument; c) better because you don't wrap a (the same) dictionary into every node, as happens with DT Contexts or GADT constructors. – AntC Jun 18 '21 at 00:50
  • "with `DataKinds` enabled, `DCNilSet` is a type, while `NilSet` isn't". Heh heh that sounds like a slam-dunk reason to prefer PatternSynonyms. – AntC Jun 18 '21 at 01:24
  • "constraints should be moved closer to the "usage site"." OK So that argues against GADT constraints. An `Eq` constraint on a `Set` is required for construction, but not necessarily for accessing, so why 'build in' a constraint on a GADT constructor? I'll post a new q with a more-specific scenario comparing GADT constructors to PatternSynonyms. – AntC Jun 18 '21 at 01:31