Skip to content

Instantly share code, notes, and snippets.

@Icelandjack

Icelandjack/ShootingStar.md

Last active August 25, 2017 14:42
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save Icelandjack/1824f4544c86b4ab497282783f94c360 to your computer and use it in GitHub Desktop.
Save Icelandjack/1824f4544c86b4ab497282783f94c360 to your computer and use it in GitHub Desktop.
Download ZIP
Playing around with GHC Trac ticket #12369
Raw
ShootingStar.md

Are these examples of

Application

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

Polynomial Functors

Products

This is very interesting because it could extend to Constraints 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

Sums

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

Like Either, Sum and Sum.

Identity

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

Void

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

Const

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

Compose

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)

Fixed Points of Functors

Reordering the arguments reveals that we have really generalized from a fixed point for kind * to a fixed point for n -> *:

Fixn :: ((n -> *) -> (n -> *)) -> (n -> *)

From bifunctors

Same is possible with things from the bifunctors package:

Join

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)

Free Functors

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.

Kan extensions

See Categories of Structures in Haskell.

Right Kan extensions

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

Left Kan extensions

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

Random stuff

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

Incomplete Ideas

Free Category

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

ZipHList (example using type function)

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)

Similar Stuff

Natural Transformations

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) }

TODO: Push it further

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.

@Icelandjack
Copy link
Author

http://www.well-typed.com/blog/2017/06/rtti/

data family RTTI (f :: k -> *) :: (k -> *)

@Icelandjack
Copy link
Author

Icelandjack commented Aug 2, 2017 •
edited

Const could be different, see Kmett's hask

newtype Const1 :: KConst Type const where
  Const :: { getConst :: ty } -> Const1 ty const

newtype Const2 :: KConst (k -> Type) const where
  Const2 :: { getConst2 :: f ty } -> Const2 f const ty

fit KConst k const = k -> const -> k and then we're like "oh this is the definition of Const3 I guess. weird"

newtype Const3 :: KConst (k -> k' -> Type) const where
  Const3 :: { getConst3 :: f ty ty' } -> Const3 f const ty ty'

"I wonder if this is also left adjoint to some hypothetical Lim3"

@Icelandjack
Copy link
Author

Icelandjack commented Aug 2, 2017 •
edited

TODO

Check if this works

type KLim k const = (const -> k) -> k

newtype Lim1 :: KLim Type const where
  Lim1 :: { getLim :: forall x. f x } -> Lim1 f

newtype Lim2 :: KLim (k -> Type) const where
  Lim2 :: { getLim2 :: forall x. f x y } -> Lim2 f y

@Icelandjack
Copy link
Author

Icelandjack commented Aug 3, 2017 •
edited 

newtype Lift0 p f g = Lift0 { lower0 :: p f g }
newtype Lift1 p f g a = Lift1 { lower1 :: p (f a) (g a) }
newtype Lift2 p f g a b = Lift2 { lower2 :: p (f a) (g a) b }

old/src/hask/core

instance Precocartesian (->) where
  type (+) = Lift0 Either

instance Precocartesian (Nat :: (i -> *) -> (i -> *) -> *) where
  type (+) = Lift1 (+)

instance Precocartesian (Nat :: (i -> j -> *) -> (i -> j -> *) -> *) where
  type (+) = Lift2 (+)

@Icelandjack
Copy link
Author

Icelandjack commented Aug 10, 2017 •
edited

For constructing dictionaries from type classes (look how revealing the kind is.. mapping type classes k -> Constraint to data types k -> Type)

data family D (f :: k -> Constraint) :: k -> Type

making something like this

data family D1 (f :: Type -> Constraint) :: Type -> Type

data instance D1 Eq a where
  DEq 
    :: (a -> a -> Bool) 
    -> D1 Eq a

data family D2 (f :: (Type -> Type) -> Constraint) :: (Type -> Type) -> Type

data instance D2 Functor f where
  DFunctor 
    :: (forall a a'. (a -> a') -> (f a -> f a')) 
    -> D2 Functor f

data family D3 (f :: (k -> k -> Type) -> Constraint) :: (k -> k -> Type) -> Type

data instance D3 Category cat where
  DCategory 
    :: (forall a. cat a a) 
    -> (forall b c a. cat b c -> cat a b -> cat a c) 
    -> D3 Category cat

but duh this is already possible! Sweet

data family D (f :: k -> Constraint) :: k -> Type

data instance D Eq a where
  DEq 
    :: (a -> a -> Bool) 
    -> D Eq a

data instance D Functor f where
  DFunctor 
    :: (forall a a'. (a -> a') -> (f a -> f a')) 
    -> D Functor f

data instance D Category cat where
  DCategory 
    :: (forall a. cat a a) 
    -> (forall b c a. cat b c -> cat a b -> cat a c) 
    -> D Category cat

@Icelandjack
Copy link
Author

TODO

http://comonad.com/reader/2015/categories-of-structures-in-haskell/

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment