[GHC] #12369: data families shouldn't be required to have return kind *, data instances should
#12369: data families shouldn't be required to have return kind *, data instances should -------------------------------------+------------------------------------- Reporter: ekmett | Owner: Type: feature | Status: new request | Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.0.1 (Type checker) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- I'd like to be able to define {{{#!hs {-# language PolyKinds, KindSignatures, GADTs, TypeFamilies #-} data family Fix :: (k -> *) -> k newtype instance Fix f = In { out :: f (Fix f) } }}} But currently this is disallowed: {{{ Fix.hs:2:1: error: • Kind signature on data type declaration has non-* return kind (k -> *) -> k • In the data family declaration for ‘Fix’ }}} Ultimately I think the issue here is that data __instances__ should be required to end in kind *, not the families, but this generalization didn't mean anything until we had `PolyKinds`. As an example of a usecase, with the above, I could define a bifunctor fixed point such as {{{#!hs newtype instance Fix f a = In2 { out2 :: f (Fix f a) a } }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12369 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12369: data families shouldn't be required to have return kind *, data instances should -------------------------------------+------------------------------------- Reporter: ekmett | Owner: Type: feature request | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Interesting idea. I can't see a technical problem with it, so maybe we could just allow it. If someone would like to have a go, I'd be a willing reviewer. Alternatively, if it becomes Important to a bunch of people, I could have a go myself. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12369#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12369: data families shouldn't be required to have return kind *, data instances should -------------------------------------+------------------------------------- Reporter: ekmett | Owner: Type: feature request | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * cc: Iceland_jack (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12369#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12369: data families shouldn't be required to have return kind *, data instances should -------------------------------------+------------------------------------- Reporter: ekmett | Owner: Type: feature request | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Is this another example of this {{{#!hs type f ~> g = forall a. f a -> g a type f ~~> g = forall a b. f a b -> g a b newtype Free0 :: Foo Type where Free0 :: (forall q. k q => (p -> q) -> q) -> Free0 k p newtype Free1 :: ((k -> Type) -> Constraint) -> (k -> Type) -> (k -> Type) where Free1 :: (forall q. k q => (p ~> q) -> q a) -> Free1 k p a newtype Free2 :: ((k1 -> k2 -> Type) -> Constraint) -> (k1 -> k2 -> Type) -> (k1 -> k2 -> Type) where Free2 :: (forall q. k q => (p ~~> q) -> q a b) -> Free2 k p a b }}} They all follow the pattern `type FREE ĸ = (ĸ -> Constraint) -> (ĸ -> ĸ)` {{{#!hs Free0 :: FREE Type Free1 :: FREE (k -> Type) Free2 :: FREE (k1 -> k2 -> Type) }}} Maybe you could write it as? {{{#!hs data family Free :: FREE k newtype instance Free :: FREE Type where Free0 :: (forall q. k q => (p -> q) -> q) -> Free k p newtype instance Free :: forall k. FREE (k -> Type) where Free1 :: (forall q. k q => (p ~> q) -> q a) -> Free k p a newtype instance Free :: forall k1 k2. FREE (k1 -> k2 -> Type) where Free2 :: (forall q. k q => (p ~~> q) -> q a b) -> Free2 k p a b }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12369#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
**Definition 2.** In Haskell, mutually recursive types can be modelled as follows.
{{{#!hs newtype Fix_1 f1 f2 = In_1 (f1 (Fix_1 f1 f2) (Fix_2 f1 f2)) newtype Fix_2 f1 f2 = In_2 (f2 (Fix_1 f1 f2) (Fix_2 f1 f2)) }}}
Since Haskell has no concept of pairs on the type level, that is, no
#12369: data families shouldn't be required to have return kind *, data instances
should
-------------------------------------+-------------------------------------
Reporter: ekmett | Owner:
Type: feature request | Status: new
Priority: normal | Milestone: 8.2.1
Component: Compiler (Type | Version: 8.0.1
checker) |
Resolution: | Keywords:
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Iceland_jack):
Should it be
{{{#!hs
type FIX k = (* -> k) -> k
data family Fix :: FIX k
}}}
which fits the type of `newtype Fix2 f a = In2 (f (Fix2 f a) a)`
{{{#!hs
Fix2 :: FIX (k -> Type)
}}}
or
{{{#!hs
type FIX k = (k -> k) -> k
data family Fix :: FIX k
}}}
which fits `newtype Fix_ f a = In_ (f (Fix_ f) a)`'s type
{{{#!hs
Fix_ :: FIX (k -> Type)
}}}
I would be **very** interested if this somehow tied in with the example of
a fixed point of mutually recursive types from
[http://www.cs.ox.ac.uk/ralf.hinze/publications/SCP-78-11.pdf s]
product kinds, we have to curry the type constructors: `Fix_1 f1 f2 = Outl
(Fix
#12369: data families shouldn't be required to have return kind *, data instances should -------------------------------------+------------------------------------- Reporter: ekmett | Owner: Type: feature request | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): [http://cs.brynmawr.edu/~rae/papers/2016/thesis/eisenberg-thesis-draft.pdf Eisenberg]:
A ''data family'' defines a family of datatypes. An example shows best how this works:
{{{#!hs data family Array a -- compact storage of elements of type a data instance Array Bool = MkArrayBool ByteArray data instance Array Int = MkArrayInt (Vector Int) }}}
With such a definition, we can have a different runtime representation for `Array Bool` than we do for `Array Int`, something not possible with more traditional parameterized types.
The part about **runtime representation** made me wonder if you could define {{{#!hs -- × × × FAILS × × × data family Array a :: TYPE rep }}} I dunno about the instances, maybe using [https://ghc.haskell.org/trac/ghc/wiki/UnliftedDataTypes#Proposal3:Allownewty... Proposal 3: Allow newtypes over unlifted types] {{{#!hs newtype instance Array Int# :: TYPE PtrRepUnlifted where MkInt# :: ByteArray# -> Array Int# newtype instance Array (##) :: TYPE IntRep where MkInt# :: Int# -> Array (##) }}} I don't really understand representation polymorphism, may suffer from same problem as #11471. ---- {{{#!hs -- WORKS FINE data family Array (a :: TYPE rep) :: Type -- × × × FAILS × × × -- -- Unexpected type ‘Int#’ data Array Int# -- Should this fail? }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12369#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12369: data families shouldn't be required to have return kind *, data instances should -------------------------------------+------------------------------------- Reporter: ekmett | Owner: Type: feature request | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Replying to [comment:5 Iceland_jack]:
The part about **runtime representation** made me wonder if you could
define
{{{#!hs -- × × × FAILS × × × data family Array a :: TYPE rep }}}
I dunno about the instances, maybe using
[https://ghc.haskell.org/trac/ghc/wiki/UnliftedDataTypes#Proposal3:Allownewty... Proposal 3: Allow newtypes over unlifted types] While there's nothing very wrong about the data family definition, the instances would be a problem, because we don't yet have a way to make user-written unlifted types. It would indeed be useful to have this, but we don't. So I think this kind of construct is best off waiting until we solve the simpler case of normal unlifted datatypes before we try unlifted data families.
----
{{{#!hs -- WORKS FINE data family Array (a :: TYPE rep) :: Type
-- × × × FAILS × × × -- -- Unexpected type ‘Int#’ data Array Int# -- Should this fail? }}}
You just want to say `data instance Array Int#`, which indeed works fine. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12369#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12369: data families shouldn't be required to have return kind *, data instances should -------------------------------------+------------------------------------- Reporter: ekmett | Owner: Type: feature request | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Replying to [comment:6 goldfire]:
So I think this kind of construct is best off waiting until we solve the simpler case of normal unlifted datatypes before we try unlifted data families.
Awesome! Maybe you can combine them into fixed point that is rep-poly ;)
You just want to say `data instance Array Int#`, which indeed works fine.
Haha oops. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12369#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12369: data families shouldn't be required to have return kind *, data instances should -------------------------------------+------------------------------------- Reporter: ekmett | Owner: Type: feature request | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: => TypeInType Comment: The stuff about representation-polymorphism is a bit of a red herring; make a new ticket. Let's not lose track of the original request here, which is well described in the Description. Richard: it might need no more than ''removing'' a test, namely the test that data families return *? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12369#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12369: data families shouldn't be required to have return kind *, data instances should -------------------------------------+------------------------------------- Reporter: ekmett | Owner: Type: feature request | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Replying to [comment:8 simonpj]:
''[...]'', make a new ticket.
#12766 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12369#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12369: data families shouldn't be required to have return kind *, data instances should -------------------------------------+------------------------------------- Reporter: ekmett | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): To avoid clutter I will add further examples to this [https://gist.github.com/Icelandjack/1824f4544c86b4ab497282783f94c360 gist]. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12369#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12369: data families shouldn't be required to have return kind *, data instances
should
-------------------------------------+-------------------------------------
Reporter: ekmett | Owner: (none)
Type: feature request | Status: new
Priority: normal | Milestone: 8.4.1
Component: Compiler (Type | Version: 8.0.1
checker) |
Resolution: | Keywords: TypeInType
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Richard Eisenberg
#12369: data families shouldn't be required to have return kind *, data instances
should
-------------------------------------+-------------------------------------
Reporter: ekmett | Owner: (none)
Type: feature request | Status: new
Priority: normal | Milestone: 8.4.1
Component: Compiler (Type | Version: 8.0.1
checker) |
Resolution: | Keywords: TypeInType
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Richard Eisenberg
#12369: data families shouldn't be required to have return kind *, data instances should -------------------------------------+------------------------------------- Reporter: ekmett | Owner: (none) Type: feature request | Status: closed Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: indexed- | types/should_compile/T12369 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * testcase: => indexed-types/should_compile/T12369 * status: new => closed * resolution: => fixed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12369#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12369: data families shouldn't be required to have return kind *, data instances should -------------------------------------+------------------------------------- Reporter: ekmett | Owner: (none) Type: feature request | Status: closed Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: indexed- | types/should_compile/T12369 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Could this work for `Constraint`s? GHC already accepts (maybe something to do with #11715) {{{ $ ghci -ignore-dot-ghci GHCi, version 8.3.20170605: http://www.haskell.org/ghc/ :? for help Prelude> :set -XTypeInType -XTypeFamilies Prelude> import Data.Kind Prelude Data.Kind> data family COMPOSE k1 k2 k3 :: (k1 -> Type) -> (k2 -> k1) -> (k2 -> Constraint) Prelude Data.Kind> }}} but it cannot be used afaik, also fails with a return kind of `TYPE IntRep`. {{{ Prelude Data.Kind GHC.Prim GHC.Exts> data family COMPOSE k1 k2 k3 :: (k1 -> Type) -> (k2 -> k1) -> (k2 -> TYPE IntRep) <interactive>:8:1: error: • Kind signature on data type declaration has non-* return kind (k1 -> *) -> (k2 -> k1) -> k2 -> TYPE 'IntRep • In the data family declaration for ‘COMPOSE’ }}} It would be interesting to combine {{{#!hs data Compose :: (k' -> Type) -> (k -> k') -> (k -> Type) where Compose :: f (g a) -> Compose f g a data Compose2 :: (k' -> (kk -> Type)) -> (k -> k') -> (k -> (kk -> Type)) where Compose2 :: f (g a) b -> Compose2 f g a b -- ComposeC :: (k' -> Constraint) -> (k -> k') -> (k -> Constraint) class f (g a) => ComposeC f g a instance f (g a) => ComposeC f g a -- ComposeC2 :: (k' -> (kk -> Constraint)) -> (k -> k') -> (k -> (kk -> Constraint)) class f (g a) b => ComposeC2 f g a b instance f (g a) b => ComposeC2 f g a b }}} as instances of a 'data' family indexed by `Type`, `kk -> Type`, `Constraint`, `kk -> Constraint` but I'm not sure if it's meaningful {{{#!hs data family Compose (k'' :: Type) :: (k' -> k'') -> (k -> k') -> (k -> k'') data instance Compose Type :: (k' -> Type) -> (k -> k') -> (k -> Type) where Compose :: f (g a) -> Compose Type f g a -- Hijacking DatatypeContexts syntax data instance f (g a) => Compose Constraint f g a data instance f (g a) b => Compose (kk -> Constraint) f g a b }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12369#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12369: data families shouldn't be required to have return kind *, data instances should -------------------------------------+------------------------------------- Reporter: ekmett | Owner: (none) Type: feature request | Status: closed Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: indexed- | types/should_compile/T12369 Blocked By: | Blocking: Related Tickets: #14045 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: => #14045 Comment: By the way, the commit message for 4239238306e911803bf61fdda3ad356fd0b42e05 claims: {{{ - A data instance need not list all patterns, much like how a GADT-style data declaration need not list all type parameters, when a kind signature is in place. This is useful, for example, here: data family Sing (a :: k) data instance Sing :: Bool -> Type where ... }}} I just tried this recently, and that example doesn't actually work. To avoid cluttering this ticket further, I've spun this off into #14045. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12369#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC