Opened 13 months ago

Last modified 4 months ago

#12369 new feature request

data families shouldn't be required to have return kind *, data instances should

Reported by: ekmett Owned by:
Priority: normal Milestone: 8.4.1
Component: Compiler (Type checker) Version: 8.0.1
Keywords: TypeInType Cc: Iceland_jack
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

I'd like to be able to define

{-# 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

newtype instance Fix f a = In2 { out2 :: f (Fix f a) a }

Change History (11)

comment:1 Changed 13 months ago 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

comment:2 Changed 10 months ago by Iceland_jack

Cc: Iceland_jack added

comment:3 Changed 9 months ago by Iceland_jack

Is this another example of this

type f  ~> g = forall a.   f a   -> g a
type f ~~> g = forall a b. f a b -> g a b

newtype Free0 :: (Type -> Constraint) -> (Type -> 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) -> (ĸ -> ĸ)

Free0 :: FREE Type
Free1 :: FREE (k -> Type)
Free2 :: FREE (k1 -> k2 -> Type)

Maybe you could write it as?

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
Last edited 9 months ago by Iceland_jack (previous) (diff)

comment:4 Changed 9 months ago by Iceland_jack

Should it be

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)

Fix2 :: FIX (k -> Type)

or

type FIX k = (k -> k) -> k

data family Fix :: FIX k

which fits newtype Fix_ f a = In_ (f (Fix_ f) a)'s type

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 s

Definition 2. In Haskell, mutually recursive types can be modelled as follows.

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 product kinds, we have to curry the type constructors: Fix_1 f1 f2 = Outl (Fix <f1, f2>) and Fix_2 f1 f2 = Outr (Fix <f1, f2>).

We can get close to an arrow in a product category

-- Beautiful definition btw
data (×) :: Cat x -> Cat y -> Cat (x, y) where
  Prod :: c1 a a_
       -> c2 b b_
       -> (c1 × c2) '(a, b) '(a_, b_)

but the closest I've gotten to modelling an endofunctor over a product category

F <A, B> = <Nat × B, 1 + A × B>

is

type family
  F (pair :: (*, *)) :: (*, *) where
  F '(a, b) = '((Int, b), Either () (a, b))

and the desired FixProd would probably have a type like ((*, *) -> (*, *)) -> (*, *) (kinds can probably be generalised)

newtype FixProd :: FIX (*, *) where
  FixProd :: ...

Except this requires a non-Type return kind, I appreciate any pointers and if having a value of type (*, *) might ever make sense

comment:5 Changed 9 months ago by Iceland_jack

Eisenberg:

A data family defines a family of datatypes. An example shows best how this works:

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

--   × × × FAILS × × ×
data family Array a :: TYPE rep

I dunno about the instances, maybe using Proposal 3: Allow newtypes over unlifted types

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.


--   WORKS FINE
data family Array (a :: TYPE rep) :: Type

--   × × × FAILS × × ×
-- 
-- Unexpected type ‘Int#’
data Array Int#
-- Should this fail?

comment:6 in reply to:  5 ; Changed 9 months ago by goldfire

Replying to Iceland_jack:

The part about runtime representation made me wonder if you could define

--   × × × FAILS × × ×
data family Array a :: TYPE rep

I dunno about the instances, maybe using 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.


--   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.

comment:7 in reply to:  6 Changed 9 months ago by Iceland_jack

Replying to 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.

comment:8 Changed 9 months ago by simonpj

Keywords: TypeInType added

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 *?

comment:9 in reply to:  8 Changed 9 months ago by Iceland_jack

Replying to simonpj:

[...], make a new ticket.

#12766

comment:10 Changed 5 months ago by Iceland_jack

To avoid clutter I will add further examples to this gist.

This feature is starting to look very attractive.

Last edited 5 months ago by Iceland_jack (previous) (diff)

comment:11 Changed 4 months ago by bgamari

Milestone: 8.2.18.4.1

Given that 8.2.1-rc1 is imminent, I'm bumping these off to the 8.4

Note: See TracTickets for help on using tickets.