[GHC] #12045: Visible kind application
#12045: Visible kind application -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature | Status: new request | Priority: normal | Milestone: Component: Compiler | Version: 8.1 Keywords: | Operating System: Unknown/Multiple TypeApplications TypeInType | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- 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 :: * }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12045 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12045: Visible kind application -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: | TypeApplications TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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: {{{#!haskell k :: Const @Bool Int 'False -- ' k = Const 42 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12045#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12045: Visible kind application -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: | TypeApplications TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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 [http://www.cis.upenn.edu/~eir here].) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12045#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12045: Visible kind application -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Iceland_jack Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: | TypeApplications TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * owner: => Iceland_jack -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12045#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12045: Visible kind application -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Iceland_jack Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: | TypeApplications TypeInType 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: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * differential: => Phab:D2216 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12045#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12045: Visible kind application -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Iceland_jack Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: | TypeApplications TypeInType 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: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Check comment:1:ticket:12418 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12045#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12045: Visible kind application -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Iceland_jack Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: | TypeApplications TypeInType 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: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): [research.microsoft.com/en-us/um/...f/promotion-tldi12-sub.pdf Giving Haskell a Promotion]: {{{#!hs data Mu :: forall k. ((k -> Type) -> (k -> Type)) -> (k -> Type) where Roll :: f (Mu f) a -> Mu 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 Vec a n = Mu (VecF a) n` instantiates `k` to `Nat` in `Mu`, so this should work: {{{
:kind Mu Mu :: ((k -> Type) -> k -> Type) -> k -> 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 }}}
-- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12045#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12045: Visible kind application -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Iceland_jack Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: | TypeApplications TypeInType 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: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): {{{#!hs 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 {{{#!hs data Node = Unit | N data NatGraph :: Cat Node where One :: NatGraph Unit N Succ :: NatGraph N N }}} {{{#!hs one :: (FreeCat @Node NatGraph) Unit N one = liftCat One }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12045#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12045: Visible kind application -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Iceland_jack Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: | TypeApplications TypeInType 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: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * cc: RyanGlScott (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12045#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12045: Visible kind application -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Iceland_jack Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: | TypeApplications TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: 12976 | Differential Rev(s): Phab:D2216 Wiki Page: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * related: => 12976 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12045#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12045: Visible kind application -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Iceland_jack Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: | TypeApplications TypeInType 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: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * related: 12976 => -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12045#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12045: Visible kind application -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Iceland_jack Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: | TypeApplications TypeInType 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: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase1#Designquestion... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12045#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12045: Visible kind application -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Iceland_jack Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: | TypeApplications TypeInType 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: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Here are some examples that are actually useful, used with a non-standard version of [https://github.com/ekmett/hask/ hask]: {{{#!hs type Fix f = (f -> f) -> f newtype Mu1 :: Fix Type where In1 :: f (Mu1 f) -> Mu1 f newtype Mu2 :: Fix (k -> Type) where In2 :: f (Mu2 f) a -> Mu2 f a }}} If you want to reference the kind variable `k` you can write {{{#!hs -- instance Functor (Mu :: ((k -> Type) -> (k -> Type)) -> (k -> Type)) where instance Functor (Mu @k) where type Dom (Mu @k) = ... type Cod (Mu @k) = ... }}} instead of {{{#!hs 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)) }}} ---- {{{#!hs 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 {{{#!hs instance Functor (Const a :: k -> Type) where type Dom (Const a :: k -> Type) = UNIT type Cod (Const a :: k -> Type) = (->) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12045#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12045: Visible kind application -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Iceland_jack Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: | TypeApplications TypeInType 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: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): We can rewrite {{{#!hs 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 {{{#!hs type Typeable1 = Typeable @(Type -> Type) type Typeable2 = Typeable @(Type -> Type -> Type) type Typeable3 = Typeable @(Type -> Type -> Type -> Type) ... }}} which is how it appears in
{{{#!hs type Typeable1 = Typeable @(* -> *) }}} — ExplicitTypeApplication#Typekindinstantiationinclasses
-- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12045#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12045: Visible kind application -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Iceland_jack Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: | TypeApplications TypeInType | GHCProposal 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: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * keywords: TypeApplications TypeInType => TypeApplications TypeInType GHCProposal -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12045#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12045: Visible kind application -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: mnguyen Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: | TypeApplications TypeInType | GHCProposal 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: | -------------------------------------+------------------------------------- Changes (by mnguyen): * owner: Iceland_jack => mnguyen Comment: Hi, I'm My Nguyen and I'm working with Richard on this :) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12045#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12045: Visible kind application -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: mnguyen Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: | TypeApplications TypeInType | GHCProposal 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: | -------------------------------------+------------------------------------- Changes (by int-index): * cc: int-index (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12045#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12045: Visible kind application -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: mnguyen Type: feature request | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: | TypeApplications TypeInType | GHCProposal Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5229 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => patch * differential: Phab:D2216 => Phab:D5229 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12045#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12045: Visible kind application -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: mnguyen Type: feature request | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: | TypeApplications TypeInType | GHCProposal Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: 14579 Related Tickets: #15782 | Differential Rev(s): Phab:D5229 Wiki Page: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * related: => #15782 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12045#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12045: Visible kind application
-------------------------------------+-------------------------------------
Reporter: Iceland_jack | Owner: mnguyen
Type: feature request | Status: patch
Priority: normal | Milestone:
Component: Compiler | Version: 8.1
Resolution: | Keywords:
| TypeApplications TypeInType
| GHCProposal
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking: 14579
Related Tickets: #15782 | Differential Rev(s): Phab:D5229
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Richard Eisenberg
#12045: Visible kind application
-------------------------------------+-------------------------------------
Reporter: Iceland_jack | Owner: mnguyen
Type: feature request | Status: patch
Priority: normal | Milestone:
Component: Compiler | Version: 8.1
Resolution: | Keywords:
| TypeApplications TypeInType
| GHCProposal
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking: 14579
Related Tickets: #15782 | Differential Rev(s): Phab:D5229
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Richard Eisenberg
#12045: Visible kind application -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: mnguyen Type: feature request | Status: closed Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.1 Resolution: fixed | Keywords: | TypeApplications TypeInType | GHCProposal 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: 14579 Related Tickets: #15782 | Differential Rev(s): Phab:D5229 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: patch => closed * testcase: => th/T12045TH{1,2}, typecheck/should_compile/T12045a, typecheck/should_fail/T12045{b,c}, parser/should_fail/T12045d, parser/should_compile/T12045e * resolution: => fixed * milestone: => 8.8.1 Comment: Merged in [https://gitlab.haskell.org/ghc/ghc/commit/17bd163566153babbf51adaff8397f948a... 17bd163566153babbf51adaff8397f948ae363ca]. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12045#comment:22 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12045: Visible kind application
-------------------------------------+-------------------------------------
Reporter: Iceland_jack | Owner: mnguyen
Type: feature request | Status: closed
Priority: normal | Milestone: 8.8.1
Component: Compiler | Version: 8.1
Resolution: fixed | Keywords:
| TypeApplications TypeInType
| GHCProposal
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: 14579
Related Tickets: #15782 | Differential Rev(s): Phab:D5229
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Richard Eisenberg
participants (1)
-
GHC