Are these examples of
data App0 :: Type -> Type where
App0 :: a -> App0
data App1 :: (k -> Type) -> (k -> Type) where
App1 :: f a -> App1 f a
data App2 :: (k -> k' -> Type) -> (k -> k' -> Type) where
App2 :: f a b -> App2 f a b
data App3 :: (k -> k' -> k'' -> Type) -> (k -> k' -> k'' -> Type) where
App3 :: f a b c -> App3 f a b c
All of those follow the form
type ENDO a = a -> a
App0 :: ENDO Type
App1 :: ENDO (k -> Type)
App2 :: ENDO (k -> k' -> Type)
App3 :: ENDO (k -> k' -> k'' -> Type)
So can it be written
data family App (a :: k) :: k
data instance App (a :: Type) = App0 a
data instance App (f :: k -> Type) (a :: k) = App1 (f a)
data instance App (f :: k -> k' -> Type) (a :: k) (b :: k') = App2 (f a b)
data instance App (f :: k -> k' -> k'' -> Type) (a :: k) (b :: k') (c :: k'') = App3 (f a b c)
This would be cool.
Is this beyond the pale?
data family App (a :: k) :: k
data instance App (a :: k) = ? :: k
data instance App (f :: k -> k') (a :: k) = ? :: k'
data instance App (f :: k -> k' -> k'') (a :: k) (b :: k') = ? :: k''
data instance App (f :: k -> k' -> k'' -> k''') (a :: k) (b :: k') (c :: k'') = ? :: k'''
This is very interesting because it could extend to Constraint
s as well, see #13341
.
data Pair0 :: Type -> Type -> Type where
Pair0 :: a -> b -> Pair0 a b
data Pair1 :: (k -> Type) -> (k -> Type) -> (k -> Type) where
Pair1 :: f a -> g a -> (Pair1 f g) a
data Pair2 :: (k -> k' -> Type) -> (k -> k' -> Type) -> (k -> k' -> Type) where
Pair2 :: f a b -> g a b -> (Pair2 f g) a b
data Pair3 :: (k -> k' -> k'' -> Type) -> (k -> k' -> k'' -> Type) -> (k -> k' -> k'' -> Type) where
Pair3 :: f a b c -> g a b c -> (Pair3 f g) a b c
with kinds
type PAIR a = a -> a -> a
Pair0 :: PAIR Type
Pair1 :: PAIR (k -> Type)
Pair2 :: PAIR (k -> k' -> Type)
Pair3 :: PAIR (k -> k' -> k'' -> Type)
Akin to (,)
, Product
, Product
/ Plus2
etc.
Could be unified with a single data family:
data family (,) :: PAIR k
-- PAIR Type
data instance (,) a b = (,) a b
-- PAIR (k -> Type)
data instance (f, g) a = Pair (f a) (g a)
-- PAIR (k -> k' -> Type)
data instance (f, g) a b = Pair2 (f a b) (g a b)
-- PAIR (k -> Constraint)
class (f a, g a) => (f, g) a
instance (f a, g a) => (f, g) a
-- PAIR (k -> k' -> Constraint)
class (f a b, g a b) => (f, g) a b
instance (f a b, g a b) => (f, g) a b
data family Sum (f :: k) (g :: k) :: k
data instance Sum (a :: Type) (b :: Type) where
Left :: a -> Sum a b
Right :: b -> Sum a b
data instance Sum (f :: k -> Type) (g :: k -> Type) (a :: k) where
InL :: f a -> (Sum f g) a
InR :: g a -> (Sum f g) a
data instance Sum (f :: k -> k' -> Type) (g :: k -> k' -> Type) (a :: k) (b :: k') where
L2 :: f a b -> (Sum f g) a b
R2 :: g a b -> (Sum f g) a b
data instance Sum (f :: k -> k' -> k'' -> Type) (g :: k -> k' -> k'' -> Type) (a :: k) (b :: k') (c :: k'') where
L3 :: f a b c -> (Sum f g) a b c
R3 :: g a b c -> (Sum f g) a b c
data family Id (a :: Type) :: k
data instance Id (a :: Type) = Id0 a
data instance Id (a :: Type) (x :: k) = Id1 a
data instance Id (a :: Type) (x :: k) (y :: k') = Id2 a
data instance Id (a :: Type) (x :: k) (y :: k') (z :: k'') = Id3 a
data family Void :: forall k. k
data instance Void :: Type
data instance Void (a :: k) :: Type
data instance Void (a :: k) (b :: k') :: Type
data instance Void (a :: k) (b :: k') (c :: k'') :: Type
data instance Void :: TYPE IntRep
data instance Void :: TYPE VoidRep
-- ???
data family Const (a :: Type) :: k
data instance Const (a :: Type) (x :: k) = Const0 a
data instance Const (a :: Type) (x :: k) (y :: k') = Const1 a
data instance Const (a :: Type) (x :: k) (y :: k') (z :: k'') = Const2 a
Basically this issue.
newtype family Compose (k -> xx) -> (k' -> k) -> (k' -> xx)
-- Compose :: (k -> Type) -> (k' -> k) -> (k' -> Type)
newtype instance Compose f g a = Compose (f (g a))
-- Compose :: (k -> k'' -> Type) -> (k' -> k) -> (k' -> k'' -> Type)
newtype instance Compose f g a b = Compose2 (f (g a) b)
-- Compose :: (k -> k'' -> k''' -> Type) -> (k' -> k) -> (k' -> k'' -> k''' -> Type)
newtype instance Compose f g a b c = Compose3 (f (g a) b c)
Reordering the arguments reveals that we have really generalized from a fixed point for kind
*
to a fixed point forn -> *
:Fixn :: ((n -> *) -> (n -> *)) -> (n -> *)
Same is possible with things from the bifunctors package:
data family Join (f :: k) :: k1
data instance Join (f :: k -> Type) (a :: k) = Join0 (f a)
data instance Join (f :: k -> k -> Type) (a :: k) = Join1 (f a a)
data instance Join (f :: k -> k -> k -> Type) (a :: k) = Join2 (f a a a)
See Categories of Structures in Haskell.
From free-functors
type FREE k = (k -> Constraint) -> (k -> k)
Free :: FREE Type
HFree :: FREE (k -> Constraint)
HHFree :: FREE (k -> k' -> Constraint)
It would looks like this
type f ~> g = forall x. f x -> g x
type f ~~> g = forall x y. f x y -> g x y
data family Free (c :: k -> Constraint) :: k -> k
data instance Free (c :: Type -> Constraint) (a :: Type) where
Free :: (forall b. c b => (a -> b) -> b) -> (Free c) a
data instance Free (c :: (k -> Type) -> Contraint) (f :: k -> Type) (a :: k) where
HFree :: (forall g. c g => (f ~> g) -> g a) -> (Free c) f a
data instance Free (c :: (k -> k' -> Type) -> Contraint) (f :: k -> k' -> Type) (a :: k) (b :: k') where
HHFree :: (forall g. c g => (f ~~> g) -> g a b) -> (Free c f) a b
etc.
See Categories of Structures in Haskell.
data family Ran (f :: k) (g :: k) :: Type -> Type
data instance Ran (f :: Type) (g :: Type) (a :: Type) where
Ran0 :: ((a -> f) -> g) -> Ran f g a
data instance Ran (f :: k -> Type) (g :: k -> Type) (a :: Type) where
Ran1 :: (forall (xx :: k). (a -> f xx) -> g xx) -> Ran f g a
data instance Ran (f :: k -> k' -> Type) (g :: k -> k' -> Type) (a :: Type) where
Ran2 :: (forall (xx :: k) (yy :: k'). (a -> f xx yy) -> g xx yy) -> Ran f g a
data instance Ran (f :: k -> k' -> k'' -> Type) (g :: k -> k' -> k'' -> Type) (a :: Type) where
Ran3 :: (forall (xx :: k) (yy :: k') (zz :: k''). (a -> f xx yy zz) -> g xx yy zz) -> Ran f g a
data family Lan (f :: k) (g :: k) :: Type -> Type
data instance Lan (f :: Type) (g :: Type) (a :: Type) where
Lan0 :: (f -> a) -> g -> (Lan f g) a
data instance Lan (f :: k -> Type) (g :: k -> Type) (a :: Type) where
Lan1 :: (f xx -> a) -> g xx -> (Lan f g) a
data instance Lan (f :: k -> k' -> Type) (g :: k -> k' -> Type) (a :: Type) where
Lan2 :: (f xx yy -> a) -> g xx yy -> (Lan f g) a
data instance Lan (f :: k -> k' -> k'' -> Type) (g :: k -> k' -> k'' -> Type) (a :: Type) where
Lan3 :: (f xx yy zz -> a) -> g xx yy zz -> (Lan f g) a
data family Random (ctx :: k -> Constraint) :: k
data instance Random (ctx :: Type -> Constraint) where
Rand0 :: ctx a => a -> Rand ctx
data instance Random (ctx :: (k -> Type) -> Constraint) (a :: k) where
Rand1 :: ctx f => f a -> (Rand ctx) a
data instance Random (ctx :: (k -> k' -> Type) -> Constraint) (a :: k) (b :: k') where
Rand2 :: ctx f => f a b -> (Rand ctx) a b
data instance Random (ctx :: (k -> k' -> k'' -> Type) -> Constraint) (a :: k) (b :: k') (c :: k'') where
Rand3 :: ctx f => f a b c -> (Rand ctx) a b c
Similar to NP
I forget if this is defined somewhere
data family AppMany (fs :: [k]) :: k
data instance AppMany (fs :: [Type]) where
Nil0 :: AppMany '[]
Cons0 :: f -> AppMany fs -> AppMany (f:fs)
data instance AppMany (fs :: [k -> Type]) (a :: k) where
Nil1 :: AppMany '[] a
Cons1 :: f a -> AppMany fs a -> AppMany (f:fs) a
data instance AppMany (fs :: [k -> k' -> Type]) (a :: k) (b :: k') where
Nil2 :: AppMany '[] a b
Cons2 :: f a b -> AppMany fs a b -> AppMany (f:fs) a b
data instance AppMany (fs :: [k -> k' -> k' -> Type]) (a :: k) (b :: k') (c :: k'') where
Nil3 :: AppMany '[] a b c
Cons3 :: f a b c -> AppMany fs a b c -> AppMany (f:fs) a b c
Similar to NS
data family AppSome (fs :: [k]) :: k
data instance AppSome (fs :: [Type]) where
Z0 :: f -> AppSome (f:fs)
S0 :: AppSome fs -> AppSome (f:fs)
data instance AppSome (fs :: [k -> Type]) (a :: k) where
Z1 :: f a -> AppSome (f:fs) a
S1 :: AppSome fs a -> AppSome (f:fs) a
data instance AppSome (fs :: [k -> k' -> Type]) (a :: k) (b :: k') where
Z2 :: f a b -> AppSome (f:fs) a b
S2 :: AppSome fs a b -> AppSome (f:fs) a b
data instance AppSome (fs :: [k -> k' -> k'' -> Type]) (a :: k) (b :: k') (c :: k'') where
Z3 :: f a b c -> AppSome (f:fs) a b c
S3 :: AppSome fs a b c -> AppSome (f:fs) a b c
Thrist lists (more info in this reddit thread), a.k.a. type-aligned sequences, a.k.a. free categories, a.k.a. path categories.
There is probably some more interesting generalisation, but this seems to generalise lists. Feedback welcome.
data family TList (f :: k) :: k
data instance TList (a :: Type) where
Nil0 :: TList a
Cons1 :: a -> TList a -> TList a
data instance TList (f :: k -> Type) (a :: k) where
Nil1 :: TList f a
Cons1 :: f a -> TList f a -> TList f a
data instance TList (cat :: CAT k) (a :: k) (b :: k) where
Nil2 :: TList cat a a
Cons2 :: cat a b -> TList cat b c -> TList cat a c
-- ???
data instance TList (f :: k -> k -> k -> Type) (a :: k) (b :: k) (c :: k)
given
type CAT k = k -> k -> Type
From this comment.
Something like this
type family
Listify ty where
Listify (a -> b) = [a] -> Listify b
Listify a = a
Then
data ZipHList0 :: [Type] -> Type where
ZipNil0 :: ZipHList0 '[]
ZipCons0 :: a -> ZipHList0 as -> ZipHList0 (a:as)
data ZipHList1 :: [k -> Type] -> ([k] -> Type) where
ZipNil1 :: ZipHList1 '[] '[]
ZipCons1 :: f a -> ZipHList1 fs as -> ZipHList1 (f:fs) (a:as)
data ZipHList2 :: [k -> k' -> Type] -> ([k] -> [k'] -> Type) where
ZipNil2 :: ZipHList2 '[] '[] '[]
ZipCons2 :: f a b -> ZipHList2 fs as bs -> ZipHList2 (f:fs) (a:as) (b:bs)
Gives types that seem to work almost
type ZIPHLIST k = [k] -> Listify k
ZipHList0 :: ZIPHLIST Type
ZipHList1 :: ZIPHLIST (k -> Type)
ZipHList2 :: ZIPHLIST (k -> k' -> Type)
This works fine with a Type
return type
data family Nat (f :: k) (g :: k) :: Type
data instance Nat (a :: Type) (b :: Type) = Nat0 (a -> b)
data instance Nat (f :: k -> Type) (g :: k -> Type) = Nat1 (forall (xx :: k). f xx -> g xx)
data instance Nat (f :: k -> k' -> Type) (g :: k -> k' -> Type) = Nat2 (forall (xx :: k) (yy :: k'). f xx yy -> g xx yy)
data instance Nat (f :: k -> k' -> k'' -> Type) (g :: k -> k' -> k'' -> Type) = Nat2 (forall (xx :: k) (yy :: k') (zz :: k''). f xx yy zz -> g xx yy zz)
but I haven't looked into how to make use of it. It has the right shape for a category
type CAT k = k -> k -> Type
Nat :: CAT Type
Nat :: CAT (k -> Type)
Nat :: CAT (k -> k' -> Type)
Maybe I'm missing something,
instance Category (Nat :: CAT k) where
I can create a type class that dispatches on kinds but I lose the inductive structure (this would be so much better with visible kind application #12045
):
class FakeCat kind where
data Nat (f :: kind) (g :: kind) :: Type
i :: (Nat :: kind -> kind -> Type) a a
c :: (Nat :: kind -> kind -> Type) b c
-> Nat a b
-> Nat a c
instance FakeCat Type where
data Nat (a :: Type) (b :: Type) = Nat0 (a -> b)
i = Nat0 id
c (Nat0 f) (Nat0 g) = Nat0 (f . g)
instance FakeCat (k -> Type) where
data Nat (f :: k -> Type) (g :: k -> Type) = Nat1 (forall xx. f xx -> g xx)
i = Nat1 id
c (Nat1 f) (Nat1 g) = Nat1 (f . g)
instance FakeCat (k -> k' -> Type) where
data Nat (f :: k -> k' -> Type) (g :: k -> k' -> Type) = Nat2 (forall xx yy. f xx yy -> g xx yy)
i = Nat2 id
c (Nat2 f) (Nat2 g) = Nat2 (f . g)
instance FakeCat (k -> k' -> k'' -> Type) where
data Nat (f :: k -> k' -> k'' -> Type) (g :: k -> k' -> k'' -> Type) = Nat3 (forall xx yy zz. f xx yy zz -> g xx yy zz)
i = Nat3 id
c (Nat3 f) (Nat3 g) = Nat3 (f . g)
and now we can define a straight-forward Category
instance branching on the kind of the natural transformation:
instance FakeCat kind => Category (Nat :: kind -> kind -> Type) where
id = i
(.) = c
Haven't given thought to how it compares to hask.
ADDED: Maybe this
type family ST :: (* -> k) -> * -> k
type instance ST = ST0
-- ST :: (* -> *) -> * -> *
newtype ST0 f s = ST1 { runST1 :: ST s (f s) }
Given :++:
data (:++:) :: (a -> Type) -> (b -> Type) -> (Either a b -> Type) where
InLL :: f a -> (f :++: g) (Left a)
InRR :: g b -> (f :++: g) (Right b)
we could index the kinds by a lifted sum over functors
data (:+++:) :: (f a -> Type) -> (g a -> Type) -> ((Sum f g) a -> Type) where
InLL2 :: f a -> (f :+++: g) (InL a)
InRR2 :: g b -> (f :+++: g) (InR b)
And so forth. See it this works once this feature gets released.
This is interesting, from Embedding Session Types in Haskell
Useful? Let's poke around