Opened 17 months ago

Last modified 7 months ago

#12045 new feature request

Visible kind application

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

Description

I've wanted this for a while

ghci> :kind (:~:)
(:~:) :: k -> k -> Type
ghci> :kind (:~:) @(Type -> Type)
(:~:) @(Type -> Type) :: (Type -> Type) -> (Type -> Type) -> Type

ghci> :kind (:~:) @(Type -> Type) []
(:~:) @(Type -> Type) [] :: (Type -> Type) -> Type

ghci> :kind (:~:) @(Type -> Type) [] Maybe
(:~:) @(Type -> Type) [] Maybe :: Type

Working like

ghci> type Same k (a::k) (b::k) = a :~: b
ghci> :kind Same
Same :: forall k -> k -> k -> *
ghci> :kind Same (Type -> Type)
Same (Type -> Type) :: (Type -> Type) -> (Type -> Type) -> *
ghci> :kind Same (Type -> Type) []
Same (Type -> Type) [] :: (Type -> Type) -> *
ghci> :kind Same (Type -> Type) [] Maybe
Same (Type -> Type) [] Maybe :: *

Change History (13)

comment:1 Changed 17 months ago by Iceland_jack

I had better motivating examples in mind way back when.

I believe this should be fine wrt parsing @ at the type level:

k :: Const @Bool Int 'False -- '
k = Const 42

comment:2 Changed 17 months ago by goldfire

This is one of the great many things I would love to work on if I had time.

Popping up a level: you've written a great many bug reports / feature requests recently. These are very helpful! Thanks! A good deal of them would naturally fall to me to implement/fix, but I'm dreadfully short of time these days. (And will be until September, at least.) So: Would you care to try to fix some of these infelicities? You have a great grasp of GHC's type system and how to abuse it (I mean that, quite surely, as a compliment), and I imagine you would have fun getting into the gearbox and getting your hands dirty.

I conjecture that this ticket is actually a good place to start. My rule of thumb is that writing a new feature is easier than debugging someone else's mistake. For a user-facing feature like this, just start by extending the abstract syntax (in hsSyn/HsType.hs, to be specific), add some rules to the parser, and then follow the errors / warnings that ensue. Unlike adding TypeApplications to expressions, the type-level type checker (er, kind checker) already does lazy instantiation, so this shouldn't be a terribly invasive change.

I'm quite happy to advise, even being short of time. One mode of collaboration might be to start a patch and submit it to Phabricator, and then I can offer feedback.

(PS: I sometimes let tickets / Phab requests slip by me these days. If you want to be sure to get a response to something, email me. My contact info is here.)

comment:3 Changed 17 months ago by Iceland_jack

Owner: set to Iceland_jack

comment:4 Changed 17 months ago by Iceland_jack

Differential Rev(s): ​Phab:D2216

comment:5 Changed 14 months ago by Iceland_jack

comment:6 Changed 13 months ago by Iceland_jack

Giving Haskell a Promotion:

data Mu :: forall k. ((k -> Type) -> (k -> Type)) -> (k -> Type) where 
  Roll :: f (Mu f) a -> Mu f a

data ListF :: (Type -> Type) -> (Type -> Type) where
  Nil  :: ListF f a
  Cons :: a -> f a -> ListF f a

data VecF :: Type -> (Nat -> Type) -> (Nat -> Type) where
  VFNil  :: VecF a f Zero
  VFCons :: a -> f n -> VecF a f (Succ n)

Applying type List a = Mu ListF a instantiates k to Type and type Vec a n = Mu (VecF a) n instantiates k to Nat in Mu:

>>> :kind Mu
Mu :: ((k -> Type) -> k -> Type) -> k -> Type

>>> :kind Mu @Type
Mu @Type :: ((Type -> Type) -> Type -> Type) -> Type -> Type

>>> :kind Mu @Type ListF
Mu @Type ListF :: Type -> Type

>>> :kind Mu @Nat
Mu @Nat :: ((Nat -> Type) -> Nat -> Type) -> Nat -> Type

>>> :kind forall a. Mu @Nat (VecF a)
forall a. Mu @Nat (VecF a) :: Nat -> Type
Last edited 13 months ago by Iceland_jack (previous) (diff)

comment:7 Changed 13 months ago by Iceland_jack

type Cat k = k -> k -> Type

data FreeCat :: Cat k -> Cat k where
  Nil  :: FreeCat f a a
  Cons :: f a b -> FreeCat f b c -> FreeCat f a c

liftCat :: f a b -> FreeCat f a b
liftCat x = Cons x Nil

Free category generated by graph of natural numbers

data Node = Unit | N

data NatGraph :: Cat Node where
  One  :: NatGraph Unit N
  Succ :: NatGraph N    N
one :: (FreeCat @Node NatGraph) Unit N
one = liftCat One

comment:8 Changed 11 months ago by RyanGlScott

Cc: RyanGlScott added

comment:9 Changed 9 months ago by Iceland_jack

comment:10 Changed 9 months ago by Iceland_jack

comment:11 Changed 9 months ago by Iceland_jack

https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase1#Designquestions


-- (~>)    :: forall k. Cat (k -> Type)
-- (~>) @N ::           Cat (N -> Type)
type f ~> g = forall a. f a -> g a

data N = O | S N

data Vec :: Type -> N -> Type where
  VNil  :: Vec a O
  VCons :: a -> Vec a n -> Vec a (S n)

vmap :: (a -> a') -> (Vec a ~> Vec a')
vmap f = \case
  VNil       -> VNil
  VCons x xs -> VCons (f x) (vmap f xs)

This should work vmap :: (a -> a') -> (Vec a ~> @N Vec a') if we allow infix à la #12363.

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

comment:12 Changed 9 months ago by Iceland_jack

Here are some examples that are actually useful, used with a non-standard version of hask:

type Fix f = (f -> f) -> f

newtype Mu1 :: Fix Type where
  In1 :: f (Mu1 f) -> Mu1 f

newtype Mu2 :: forall k. Fix (k -> Type) where
  In2 :: f (Mu2 f) a -> Mu2 f a

If you want to reference the kind variable k you can write

-- instance Functor (Mu :: forall k. ((k -> Type) -> (k -> Type)) -> (k -> Type)) where
instance Functor (Mu @k) where
  type Dom (Mu @k) = ...
  type Cod (Mu @k) = ...

instead of

instance Functor (Mu :: Fix (k -> Type)) where
  type Dom (Mu :: Fix (k -> Type)) = (Void :: Cat ((k -> Type) -> (k -> Type)))
  type Cod (Mu :: Fix (k -> Type)) = (Void :: Cat (k -> Type))

instance Functor (Const @k a) where
  type Dom (Const @k a) = UNIT
  type Cod (Const @k a) = (->)

  fmap :: UNIT b b' -> (Const a b -> Const a b')
  fmap UNIT (Const a) = Const a

instead of

instance Functor (Const a :: k -> Type) where
  type Dom (Const a :: k -> Type) = UNIT
  type Cod (Const a :: k -> Type) = (->)
Last edited 9 months ago by Iceland_jack (previous) (diff)

comment:13 Changed 9 months ago by Iceland_jack

We can rewrite

type Typeable1 (a :: Type -> Type)                 = Typeable a
type Typeable2 (a :: Type -> Type -> Type)         = Typeable a
type Typeable3 (a :: Type -> Type -> Type -> Type) = Typeable a
...

as the more natural

type Typeable1 = Typeable @(Type -> Type)
type Typeable2 = Typeable @(Type -> Type -> Type)
type Typeable3 = Typeable @(Type -> Type -> Type -> Type)
...

which is how it appears in

type Typeable1 = Typeable @(* -> *)

ExplicitTypeApplication#Typekindinstantiationinclasses

Edit: gist could use Nat @kind.

Last edited 7 months ago by Iceland_jack (previous) (diff)
Note: See TracTickets for help on using tickets.