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
comment:2 Changed 17 months ago by
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
Owner: | set to Iceland_jack |
---|
comment:4 Changed 17 months ago by
Differential Rev(s): | → Phab:D2216 |
---|
comment:6 Changed 13 months ago by
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
comment:7 Changed 13 months ago by
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
Cc: | RyanGlScott added |
---|
comment:9 Changed 9 months ago by
Related Tickets: | → 12976 |
---|
comment:10 Changed 9 months ago by
Related Tickets: | 12976 |
---|
comment:11 Changed 9 months ago by
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.
comment:12 Changed 9 months ago by
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) = (->)
comment:13 Changed 9 months ago by
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 @(* -> *)
Edit: gist could use Nat @kind
.
I had better motivating examples in mind way back when.
I believe this should be fine wrt parsing
@
at the type level: