#12045 closed feature request (fixed)
Visible kind application
Reported by: | Iceland_jack | Owned by: | mnguyen |
---|---|---|---|
Priority: | normal | Milestone: | 8.8.1 |
Component: | Compiler | Version: | 8.1 |
Keywords: | TypeApplications TypeInType GHCProposal | Cc: | RyanGlScott, int-index |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | th/T12045TH{1,2}, typecheck/should_compile/T12045a, typecheck/should_fail/T12045{b,c}, parser/should_fail/T12045d, parser/should_compile/T12045e |
Blocked By: | Blocking: | ||
Related Tickets: | #15782 | Differential Rev(s): | Phab:D5229 |
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 (24)
comment:1 Changed 3 years ago by
comment:2 Changed 3 years 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 3 years ago by
Owner: | set to Iceland_jack |
---|
comment:4 Changed 3 years ago by
Differential Rev(s): | → Phab:D2216 |
---|
comment:6 Changed 3 years 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 3 years 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 3 years ago by
Cc: | RyanGlScott added |
---|
comment:9 Changed 3 years ago by
Related Tickets: | → 12976 |
---|
comment:10 Changed 3 years ago by
Related Tickets: | 12976 |
---|
comment:11 Changed 3 years 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 3 years 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 3 years 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
.
comment:14 Changed 16 months ago by
Keywords: | GHCProposal added |
---|
comment:15 Changed 14 months ago by
Owner: | changed from Iceland_jack to mnguyen |
---|
Hi, I'm My Nguyen and I'm working with Richard on this :)
comment:16 Changed 14 months ago by
Cc: | int-index added |
---|
comment:17 Changed 11 months ago by
Differential Rev(s): | Phab:D2216 → Phab:D5229 |
---|---|
Status: | new → patch |
comment:18 Changed 11 months ago by
Blocking: | 14579 added |
---|
comment:19 Changed 11 months ago by
Related Tickets: | → #15782 |
---|
comment:22 Changed 9 months ago by
Milestone: | → 8.8.1 |
---|---|
Resolution: | → fixed |
Status: | patch → closed |
Test Case: | → th/T12045TH{1,2}, typecheck/should_compile/T12045a, typecheck/should_fail/T12045{b,c}, parser/should_fail/T12045d, parser/should_compile/T12045e |
Merged in 17bd163566153babbf51adaff8397f948ae363ca:
Author: mynguyen <mnguyen1@brynmawr.edu> Date: Tue Dec 18 11:52:26 2018 -0500 Visible kind application Summary: This patch implements visible kind application (GHC Proposal 15/#12045), as well as #15360 and #15362. It also refactors unnamed wildcard handling, and requires that type equations in type families in Template Haskell be written with full type on lhs. PartialTypeSignatures are on and warnings are off automatically with visible kind application, just like in term-level. There are a few remaining issues with this patch, as documented in ticket #16082. Includes a submodule update for Haddock. Test Plan: Tests T12045a/b/c/TH1/TH2, T15362, T15592a Reviewers: simonpj, goldfire, bgamari, alanz, RyanGlScott, Iceland_jack Subscribers: ningning, Iceland_jack, RyanGlScott, int-index, rwbarton, mpickering, carter GHC Trac Issues: `#12045`, `#15362`, `#15592`, `#15788`, `#15793`, `#15795`, `#15797`, `#15799`, `#15801`, `#15807`, `#15816` Differential Revision: https://phabricator.haskell.org/D5229
comment:24 Changed 8 months ago by
Blocking: | 14579 removed |
---|
I had better motivating examples in mind way back when.
I believe this should be fine wrt parsing
@
at the type level: