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

Authored by Iceland_jack on May 25 2016, 8:52 PM.

Details

Summary

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

Diff Detail

Repository
rGHC Glasgow Haskell Compiler
Lint
Automatic diff as part of commit; lint not applicable.
Unit
Automatic diff as part of commit; unit tests not applicable.
Iceland_jack retitled this revision from to Added type family dependency to Data.Type.Bool.Not, Trac #12057).May 25 2016, 8:52 PM
Iceland_jack updated this object.
Iceland_jack edited the test plan for this revision. (Show Details)
Iceland_jack added a reviewer: goldfire.
Iceland_jack updated the Trac tickets for this revision.

Fixed GHC range.

Hm, it looks like something messed up when the Diff was updated, since this only shows the changes in the last commit. Can you rebase your changes on top of master and arc diff --update D2268?

Also, base is built as a stage-2 dependency (i.e., with the latest GHC), so you can use TypeFamilyDependencies unconditionally.

I don't like VC.

RyanGlScott requested changes to this revision.May 25 2016, 9:31 PM
RyanGlScott added a reviewer: RyanGlScott.

Looks good! A couple of minor things:

First, make sure to add an entry to base's changelog describing this change (and Trac ticket number).

libraries/base/Data/Type/Bool.hs
51–54

You don't really need to put Trac tickets in user-facing Haddocks, since they're mostly for developer reference. In fact, I'd opt to keep the documentation as it is, since Haddock will render type famiky dependencies anyway.

This revision now requires changes to proceed.May 25 2016, 9:31 PM

What do you think about

-- | Injective /since: ???/

Updated changelog.md.

These are other potential type family dependencies I found.

From original paper, so I guess this should be added:

-- ./libraries/vector/Data/Vector/Generic/Base.hs
type family Mutable (v :: * -> *) = (res :: * -> * -> *) | res -> v
-- ./libraries/base/GHC/Generics.hs
class (kparam ~ 'KProxy) => SingKind (kparam :: KProxy k) where
  -- | Get a base type from a proxy for the promoted kind. For example,
  -- @DemoteRep ('KProxy :: KProxy Bool)@ will be the type @Bool@.
  type DemoteRep kparam = (res :: *) | res -> kparam

These are probably not super useful.

This could also be a closed type family, but since it's from old-testsuite it may not be worth changing.

-- ./libraries/vector/old-testsuite/Testsuite/Utils/Property.hs
type family Ty a = res | res -> a
-- ./libraries/hoopl/src/Compiler/Hoopl/Collections.hs
class IsSet set where
  type ElemOf set = res | res -> set

class IsMap map where
  type KeyOf map = res | res -> map

-- ./libraries/hoopl/src/Compiler/Hoopl/Unique.hs
instance IsSet UniqueSet where
  type ElemOf UniqueSet = Unique

instance IsMap UniqueMap where
  type KeyOf UniqueMap = Unique

-- ./libraries/hoopl/src/Compiler/Hoopl/Label.hs
instance IsSet LabelSet where
  type ElemOf LabelSet = Label

instance IsMap LabelMap where
  type KeyOf LabelMap = Label
RyanGlScott accepted this revision.May 26 2016, 8:09 AM

Thanks, @Iceland_jack!

As for the other suggested type families:

  • Mutable: I agree! However, vector is used as a submodule in GHC from its GitHub repo, so I'd make a PR there if you want to change it to be injective. (There's already this issue which pertains to the need for injective type families.)
  • DemoteRep: Ostensibly, this looks like it could be injective. However, you might want to make a PR to the singletons repo first (where this code was taken) to make sure there isn't some strange corner case that violates injectivity. (In any case, DemoteRep is completely internal to GHC.Generics in base, so whether it's injective or not is inconsequential.)
  • Ty: I'd avoid touching any testsuite code unless you have a very good reason to change it.
  • ElemOf/KeyOf: Looks plausible, but again, make a PR request to the hoopl GitHub repo if you want to see this change.
This revision is now accepted and ready to land.May 26 2016, 8:09 AM

What are your comments on

What do you think about

-- | Injective /since: ???/

Even though Haddock renders type family dependencies I like knowing when features were added, just as Haddock displays instances but it's still useful knowing when they were added.

austin accepted this revision.May 27 2016, 4:47 AM
austin retitled this revision from Added type family dependency to Data.Type.Bool.Not, Trac #12057) to Added type family dependency to Data.Type.Bool.Not.

Should there be a test for this? Looks OK either way.

What are your comments on

What do you think about

-- | Injective /since: ???/

Even though Haddock renders type family dependencies I like knowing when features were added, just as Haddock displays instances but it's still useful knowing when they were added.

Oops, I didn't notice that comment. I wouldn't be opposed to a comment like An injective type family /since: ???/, but I don't know at this point what to put in place of ???. @hvr?

bgamari requested changes to this revision.May 29 2016, 5:48 AM

I agree that we should have a "since" comment. @hvr, who do we want to version this?

This revision now requires changes to proceed.May 29 2016, 5:48 AM

I just noticed that the GHC 8.2.1 release notes have named the next version base-4.10.0.0. Is this accurate?

I spoke with @hvr, and he agrees that 4.10.0.0 is what we should use for now.

@Iceland_jack, can you change the Haddocks for Not to something like this?

-- | Type-level "not". An injective type family since @4.10.0.0@.
--
-- @since 4.7.0.0

(4.7.0.0 being the base version in which Not was introduced.)

By the way @Iceland_jack, I was curious about whether DemoteRep could be injective in the general case, so I tried marking it as injective in the upstream singletons repo. It turns out the answer is no:

[32 of 50] Compiling Data.Singletons.TypeLits.Internal ( src/Data/Singletons/TypeLits/Inte

src/Data/Singletons/TypeLits/Internal.hs:1:1: error:
    Type family equations violate injectivity annotation:
      DemoteRep [a0] = [DemoteRep a0]
        -- Defined in ‘Data.Singletons.TypeLits.Internal’
      DemoteRep Symbol = String
        -- Defined at src/Data/Singletons/TypeLits/Internal.hs:66:8

At least, as long as we keep the Symbol hack around.

Added information on when Not was made injective.

@Iceland_jack, I think you accidentally removed your commit that modified the changelog. (See https://phabricator.haskell.org/D2268?vs=7742&id=8201).

Added changelog.

Thanks for reminding me of this ticket @RyanGlScott

This revision was automatically updated to reflect the committed changes.