Opened 2 years ago

Closed 8 months ago

Last modified 4 weeks ago

#8026 closed feature request (wontfix)

DatatypeContexts should be fixed, not deprecated

Reported by: gidyn Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.6.3
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Revisions:

Description

To borrow an example from the prime wiki page, the following code fails to compile:

data Eq a => Foo a = Foo a

isEq :: Foo a -> Foo a -> Bool
isEq (Foo x) (Foo y) = x == y

We have to tell the compiler that Eq a => Foo a in isEq, even though this is part of the data type's definition. Furthermore,

getVal :: Foo a -> a
getVal (Foo x) = x

will also fail because of the missing constraint, even though it isn't used in the function's definition.

Rather than just deprecating the DatatypeContexts extension, it should be "fixed" to remember the context wherever the data type is used.

Change History (25)

comment:1 follow-up: Changed 2 years ago by simonpj

  • difficulty set to Unknown
  • Resolution set to wontfix
  • Status changed from new to closed

We already have a notation for the "fixed" version:

data Foo a where
  Foo :: Eq a => a -> Foo a

Moreover, this is arguably the "right" notation because you can vary the context per-constructor:

data Bar a where
  Bar1 :: Eq a => a -> Bar a
  Bar2 :: (Ix a, Show a) => a -> a -> Bar a

You may want to make suggesitons to the Haskell Prime group, but I'm disinclined to add yet new behaviour to GHC when an existing solution does the job.

Simon

comment:2 Changed 2 years ago by gidyn

  • Resolution wontfix deleted
  • Status changed from closed to new

This only works when pattern matching on the constructor, and GADTs are no different to classical data types for this. Functions which uses a Foo without pattern matching will require a redundant type context in either case.

comment:3 Changed 2 years ago by gidyn

This might be a better example:

data Eq a => Pair a = Pair {x::a, y::a}

equal :: Pair a -> Bool
equal pair = (x pair) == (y pair)

Is there any way you can avoid a redundant Eq a => in the definition of equal, without adding a redundant pattern match?

comment:4 Changed 2 years ago by gidyn

  • Cc gideon@… added

comment:5 in reply to: ↑ 1 Changed 2 years ago by gidyn

Replying to simonpj:

You may want to make suggesitons to the Haskell Prime group

Haskell Prime expect extensions to be implemented in a compiler first, so that would have to come if/after it's been implemented here.

comment:6 Changed 2 years ago by isaacdupree

In your example, do any of these three expressions typecheck? (note: functions are not in Eq)

Pair id id
undefined :: Pair (()->())
equal undefined

comment:7 follow-up: Changed 2 years ago by monoidal

@gidyn: What would the type of x be in your example?

You probably want x to introduce the validity of constraint Eq a. So the type would be somewhat dual to Eq a => Pair a -> a: using it would prove the constraint Eq a, rather than requiring evidence for the constraint. Something like Pair a -> (Eq a; a).

It seems to me this change would complicate the type system a lot, while the benefits are rather doubtful.

comment:8 in reply to: ↑ 7 Changed 2 years ago by gidyn

Replying to monoidal:

The generated getter should have type Eq a => Pair a -> a - nothing complicated about it, unless I missed your point.

Last edited 8 months ago by gidyn (previous) (diff)

comment:9 follow-up: Changed 2 years ago by monoidal

@gidyn: You probably meant x :: Eq a => Pair a -> a.

Consider isaacdupree's equal (undefined :: Pair (() -> ())). Surely this should be legal: undefined inhabits every type. Yet attempting to evaluate it leads to using == from Eq (() -> ()) which does not exist.

comment:10 follow-up: Changed 23 months ago by monoidal

  • Resolution set to wontfix
  • Status changed from new to closed

As far as I understand, the proposal is not sound.

comment:11 in reply to: ↑ 9 Changed 23 months ago by gidyn

Replying to monoidal:

Consider isaacdupree's equal (undefined :: Pair (() -> ())). Surely this should be legal: undefined inhabits every type. Yet attempting to evaluate it leads to using == from Eq (() -> ()) which does not exist.

The use of DatatypeContexts would make this equivalent to equal (undefined :: Eq ? => Pair (() -> ())), so the type he's asking about couldn't (and shouldn't) be constructed when using this extension.

Excluding some nefarious uses of undefined seems like a reasonable price to pay for turning on a useful extension.

comment:12 in reply to: ↑ 10 Changed 23 months ago by gidyn

Replying to monoidal:

As far as I understand, the proposal is not sound.

I think that there is some misunderstanding here. This is not proposing to change the actual type system, just that the DatatypeContexts extension should enable automatic context inference. This is similar to SPJ's (...) => proposal, but tied to the extension which makes requires it, and without the syntactic noise.

Version 0, edited 23 months ago by gidyn (next)

comment:13 Changed 8 months ago by yokto

I like the idea of fixing this too. The main Idea would be to hide Contexts from sight. As an example of how this could be useful consider Num were a newtype instead of a type class

newtype (Num n) => Num' n = Num' n
type Int' = Num' Int

(+) :: Num' n -> Num' n -> Num' n

This would mean you could actually make instances

instance SomeClass (Num' n)

that don't conflict with all other instances

instance (Num n) => SomeClass n
instance SomeClass Char

crash

and even if you enable ugly extensions like UndecidableInstances this can not fix your problems if you want to use type families or functional dependencies.

you can not make an instance

class SomeClass a b | a -> b

instance (Num n) => SomeClass n b

without immediately blocking all other possible Instances.

Maybe these DatatypeContexts based containers are a bit less flexible than common classes in that they don't mix, but if you know they don't have to mix it makes instances a lot easier and safer.

of course you can always add the context explicitly but it would be nice if ghc infer them. As gidyn said I don't think this would change the type system overly much. You would just get contexts that don't need not be explicitly stated. Every time you do context checks you can easily derive them from the type.

Last edited 8 months ago by yokto (previous) (diff)

comment:14 Changed 8 months ago by gidyn

  • Resolution wontfix deleted
  • Status changed from closed to new

comment:15 Changed 8 months ago by goldfire

It seems that those of us who have hacked on GHC in the past have a hard time understanding this proposal -- which, to me, looks either unsound (if implemented simply) or very complicated (adding the ability to return a constraint). If you want this to be considered, please write up a wiki page with detailed examples and types. Also, suggest how this feature should be implemented, in terms of a translation to GHC's core language. It currently all seems a little magical. Thanks!

comment:16 Changed 8 months ago by gidyn

Consider the first example

data Eq a => Foo a = Foo a

isEq :: Foo a -> Foo a -> Bool
isEq (Foo x) (Foo y) = x == y

This won't compile, because isEq is missing Eq a =>. However, if we miss out the type signature altogether, GHC will correctly infer it. With Partial Type Signatures, we can also write

isEq :: _ => Foo a -> Foo a -> Bool

and GHC will infer the constraint.

This proposal is requesting that whenever DatatypeContexts has been turned on, and a data type appears in a type signature, GHC will automatically infer the data type's context in the same way as it would for an extra-constraints wildcard.

It is different to extra-constraints wildcards in that:

  • no explicit syntax is needed, other than DatatypeContexts
  • the only constraint which can be added by inference is one that was given in the data type declaration.

Is that clearer?

Last edited 8 months ago by gidyn (previous) (diff)

comment:17 Changed 8 months ago by gidyn

To emphasise: this proposal is not proposing a change to the type system. It is, similar to ​Partial Type Signatures, proposing a new use for GHC's existing type inference capabilities.

comment:18 Changed 8 months ago by goldfire

This proposal does propose a change to the type system, as it proposes a change to the set of well-typed programs. The same is true of partial type signatures. Type inference is an algorithm that implements a way to enforce the constraints of a type system.

Your example is clear for that simple situation. But, Haskell's type system is not that simple! For example:

data Eq a => HasEq a = MkHasEq a
  deriving Typeable
data Show a => HasShow a = MkHasShow a
a :: Maybe (HasEq a) -> Maybe (HasEq a) -> Bool
a (Just x) (Just y) = x == y
a _ _ = Nothing

b :: Either (HasEq a) (HasShow a) -> String   -- what constraints are used here???
b (Left x) = show (x == x)
b (Right x) = show x

c :: Proxy (HasEq a) -> ()   -- what constraints are used here???
c _ = ()

data Dynamic = forall a. Typeable a => MkDyn a

d :: Dynamic -> Maybe Bool
d (MkDyn y) | Just (MkHasEq z) <- cast y = Just (z == z)   -- where does the Eq constraint come from??
d _ = Nothing

Your examples seem to address specific, easy cases. But, we need to consider all the wide range of compositions with other Haskell features!

comment:19 Changed 8 months ago by yokto

Ok I'm not an expert in type theory or anything but let me try to explain based on your example. I don't know how this relates to type theory or if it is sound but it covers all the cases I could think of.

data Eq a => HasEq a = MkHasEq a

Deriving Types

How can you get a value of type HasEq a.

  1. Using a Constructor (also in a pattern): Use the same trick as with GADTs? Just make the type signature of the constructor (Eq a) => a -> HasEq a
  2. Explicit type signature (undefined :: HasEq a): Add the constraint (Eq a) to all explicit type signatures containing HasEq a. If you have more variables HasEq (Either a b) use the inner most forall in which one of the variables is bound

(forall a. HasEq (Either a b) -> c) -> c -> b
becomes

(forall a. (Eq (Either a b)) => HasEq (Either a b) -> c) -> c -> b

  1. Functions in modules without this extension. Maybe it's possible to add the contexts when the functions are imported. I don't know.

Hiding Types.

This doesn't even really concern haskell anymore. It's just a question of how you can tell ghci or haddock that it doesn't need to show the contexts that were derived.

Examples

Example1:

a :: Maybe (HasEq a) -> Maybe (HasEq a) -> Bool
a (Just x) (Just y) = x == y
a _ _ = Nothing

according to rule 2. gets translated to.
a :: (Eq a) => Maybe (HasEq a) -> Maybe (HasEq a) -> Bool

Example2:

b :: Either (HasEq a) (HasShow a) -> String   -- what constraints are used here???
b (Left x) = show (x == x)
b (Right x) = show x

according to rule 2. gets translated to.
b :: (Eq a, Show a) => Either (HasEq a) (HasShow a) -> String

Example3:

c :: Proxy (HasEq a) -> ()   -- what constraints are used here???
c _ = ()

according to rule 2. gets translated to. Though I don't really know what Proxy does.
c :: (Eq a) => Proxy (HasEq a) -> ()

d :: Dynamic -> Maybe Bool
d (MkDyn y) | Just (MkHasEq z) <- cast y = Just (z == z)   -- where does the Eq constraint come from??
d _ = Nothing

according to rule 1. The Eq quality constraint gets set because of the use of the constructor. I'm not sure how to write this in terms of types but it works for GADTs.

Last edited 8 months ago by yokto (previous) (diff)

comment:20 Changed 8 months ago by gidyn

I think we actually have 2 implementation proposals here:

  • tokyo's rules add type constraints, whenever the data type appears in an explicit type signature or when the constructor is used
  • use regular type inference

The second implementation would give different results for c and d:

c :: Proxy (HasEq a) -> ()   -- what constraints are used here???
c _ = ()

No type constraint is added, because none is inferred by the definition of c.

data Dynamic = forall a. Typeable a => MkDyn a

d :: Dynamic -> Maybe Bool
d (MkDyn y) | Just (MkHasEq z) <- cast y = Just (z == z)   -- where does the Eq constraint come from??
d _ = Nothing

DatatypeContexts wouldn't have any effect in this case.

comment:21 Changed 8 months ago by yokto

I just found an other interesting realworld example that could profit from this extension. Consider the vector package. All type signature look something like this.

read :: PrimMonad m => MVector (PrimState m) a -> Int -> m a

Horrible to read, right. With this issue fixed you could put the context on MVector

data (PrimMonad m) => MVector m a = MVector !Int !Int !(MutableArray (PrimState m) a)

and the type signatures could look like this

read :: MVector m a -> Int -> m a

Actually I don't know if this would work but it looks good.

Last edited 8 months ago by yokto (previous) (diff)

comment:22 Changed 8 months ago by simonpj

I urge you to read the OutsideIn(X) paper.

I think that what you want in comment:21 is already fully implemented. You would declare MVector like this:

data MVector m a where
  MVector :: PrimMonad m 
          => !Int -> !Int -> !(MutableArray (PrimState m) a) -> MVector m a

comment:23 Changed 8 months ago by goldfire

  • Resolution set to wontfix
  • Status changed from new to closed

I'm afraid the recent salvo of examples has done little to convince me of what this extension really means. The only I can glean from this is you want a very syntactic translation of a type ... HasEq a ... to Eq a => ... HasEq a .... The problem is that this translation doesn't always make sense, given the other features of Haskell's type system, and would either work or not work in various scenarios unpredictably.

At the risk of repeating myself: those of us with experience working inside GHC and who do know type theory think this proposal doesn't fly. We love contributions and ideas from folks without this experience. But, in this case, where we disagree with the proposal, the burden rests on the proposers to convince us that the proposal holds water. The way to do this starts with a wiki page and typing rules, not just examples.

comment:24 Changed 8 months ago by yokto

Ok @simonpj, that's right. I think I was mistaken and this is not as important as I thought.

Though it there are still some cases that are not covered.

Ok, so let my try to create a wiki page. InferDatatypeContexts

Last edited 8 months ago by yokto (previous) (diff)

comment:25 Changed 4 weeks ago by gidyn

  • Cc gideon@… removed
Note: See TracTickets for help on using tickets.