Opened 3 years ago

Closed 3 years ago

#12057 closed feature request (fixed)

TypeFamilyDependencies on Data.Type.Bool's `Not`

Reported by: Iceland_jack Owned by: Iceland_jack
Priority: normal Milestone: 8.2.1
Component: libraries/base Version: 8.0.1
Keywords: TypeFamilies, Injective, newcomer Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D2268
Wiki Page:

Description

With TypeFamilyDependencies (InjectiveTypeFamilies) can't Rep from Generic have a dependency?

class Generic a where
  type Rep a = (res :: Type -> Type) | res -> a
  ...

Assuming the meta data is always unique.

Change History (13)

comment:1 Changed 3 years ago by Iceland_jack

Rep1 also

comment:2 Changed 3 years ago by Iceland_jack

Data.Type.Bool.Not can be made injective

type family Not (a :: Bool) = (res :: Bool) | res -> a
Last edited 3 years ago by Iceland_jack (previous) (diff)

comment:3 Changed 3 years ago by RyanGlScott

Rep definitely isn't injective. Counterexample: Rep (Proxy Int) = Rep (Proxy Char), but Int is not Char.

Not can certainly be made injective though, and this would be simple to do and useful. Would you care to make a patch for it?

comment:4 Changed 3 years ago by RyanGlScott

Keywords: newcomer added
Summary: TypeFamilyDependencies on GHC.Generic's `Rep`TypeFamilyDependencies on Data.Type.Bool's `Not`

comment:5 in reply to:  3 ; Changed 3 years ago by Iceland_jack

Replying to RyanGlScott:

Rep definitely isn't injective. Counterexample: Rep (Proxy Int) = Rep (Proxy Char), but Int is not Char.

Interesting, thank you. Would this be covered by the weaker ‘head’-injectivity?

Is there any benefit from adding this distinguishing information/kind information to the metadata (since Proxy is polykinded)?

I am perversely working backwards from the perspective of injectivity but there may be a use for TypeReps in the Rep.

Not can certainly be made injective though, and this would be simple to do and useful. Would you care to make a patch for it?

Sure, it can be kept open for more injective type families in base.

comment:6 Changed 3 years ago by Iceland_jack

Owner: set to Iceland_jack

comment:7 in reply to:  5 ; Changed 3 years ago by RyanGlScott

Replying to Iceland_jack:

Interesting, thank you. Would this be covered by the weaker ‘head’-injectivity?

In principle, it should be. Ever since we added packageName to the generics metadata, every Rep instance should be uniquely identified by the package, module, and datatype name of the underlying datatype, so I think Reps are unique modulo type variables.

I say "in principle" because although most Generic instances (and hence Rep instances) are derived, a devilish programmer could handwrite a Rep instance that violates injectivity. However, it's strongly discouraged to do such a thing (for instance, you can't handwrite Generic instances in Safe code), so I don't know if that would even be an issue in practice.

Is there any benefit from adding this distinguishing information/kind information to the metadata (since Proxy is polykinded)?

I am perversely working backwards from the perspective of injectivity but there may be a use for TypeReps in the Rep.

Well, I've never found myself wanting to put TypeRep in Rep precisely because Typeable's a whole 'nother can of worms, and it does feel perverse to jam more stuff into an already cluttered Rep. Furthermore, I don't think this would solve the problem of making it injective, since TypeRep values represent monomorphic types.

Sure, it can be kept open for more injective type families in base.

Out of curiosity, are there any other type families in base besides Not that can be injective?

comment:8 Changed 3 years ago by Iceland_jack

Differential Rev(s): D2268

comment:9 Changed 3 years ago by Iceland_jack

Differential Rev(s): D22682268

comment:10 Changed 3 years ago by Iceland_jack

Differential Rev(s): 2268Phab:D2268

comment:11 in reply to:  7 Changed 3 years ago by Iceland_jack

Replying to RyanGlScott:

I say "in principle" because although most Generic instances (and hence Rep instances) are derived, a devilish programmer could handwrite a Rep instance that violates injectivity.

That could be checked if GHC ends up adding support for head-injectivity, there may be use cases for an injective Rep.

Out of curiosity, are there any other type families in base besides Not that can be injective?

I can sift through base and see if there are others, posting them here.

comment:12 Changed 3 years ago by Ryan Scott <ryan.gl.scott@…>

In 37aeff63/ghc:

Added type family dependency to Data.Type.Bool.Not

Summary:

Signed-off-by: Baldur Blöndal <baldurpet@gmail.com>

Reviewers: goldfire, RyanGlScott, austin, bgamari, hvr

Reviewed By: RyanGlScott, austin

Subscribers: RyanGlScott, thomie

Differential Revision: https://phabricator.haskell.org/D2268

GHC Trac Issues: #12057

comment:13 Changed 3 years ago by RyanGlScott

Milestone: 8.2.1
Resolution: fixed
Status: newclosed
Note: See TracTickets for help on using tickets.