Opened 4 years ago

Closed 11 months ago

Last modified 10 months ago

#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 4 years 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 4 years 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 4 years ago by Iceland_jack

Owner: set to Iceland_jack

comment:4 Changed 4 years ago by Iceland_jack

Differential Rev(s): ​Phab:D2216

comment:5 Changed 3 years ago by Iceland_jack

comment:6 Changed 3 years 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 3 years ago by Iceland_jack (previous) (diff)

comment:7 Changed 3 years 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 3 years ago by RyanGlScott

Cc: RyanGlScott added

comment:9 Changed 3 years ago by Iceland_jack

comment:10 Changed 3 years ago by Iceland_jack

comment:11 Changed 3 years 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 3 years ago by Iceland_jack (previous) (diff)

comment:12 Changed 3 years 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 3 years ago by Iceland_jack (previous) (diff)

comment:13 Changed 3 years 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 3 years ago by Iceland_jack (previous) (diff)

comment:14 Changed 18 months ago by RyanGlScott

Keywords: GHCProposal added

comment:15 Changed 17 months ago by mnguyen

Owner: changed from Iceland_jack to mnguyen

Hi, I'm My Nguyen and I'm working with Richard on this :)

comment:16 Changed 16 months ago by int-index

Cc: int-index added

comment:17 Changed 13 months ago by RyanGlScott

Differential Rev(s): ​Phab:D2216Phab:D5229
Status: newpatch

comment:18 Changed 13 months ago by RyanGlScott

Blocking: 14579 added

comment:19 Changed 13 months ago by Iceland_jack

comment:20 Changed 13 months ago by Richard Eisenberg <rae@…>

In 255d2e3/ghc:

Fix embarrassing, egregious bug in roles of (->)

Previously, I had inexplicably decided that (->)'s roles
were all Representational. But, of course, its first two
parameters are *dependent* RuntimeReps. All dependent parameters
have a Nominal role, because all roles in kinds are Nominal.

Fix is easy, but I have no idea how the world hasn't come
crashing down before now.

This was found while investigating #15801, which requires
visible type application in types to observe. Hence, the test
case will come with the main patch for #12045.

comment:21 Changed 13 months ago by Richard Eisenberg <rae@…>

In 74ed9c1c/ghc:

Actually fail in failIfEmitsConstraints

The function TcHsType.failIfEmitsConstraints says that it fails.
It even does so in its name. But it didn't! It *reported* constraints
but didn't fail. Now it does.

This is important in tcHsClsInstType; see the comments therein.

This was discovered while looking at #15797, but that ticket
requires visible kind application to exhibit the bug; the test
case will come with the patch for #12045.

comment:22 Changed 11 months ago by RyanGlScott

Milestone: 8.8.1
Resolution: fixed
Status: patchclosed
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
Last edited 11 months ago by RyanGlScott (previous) (diff)

comment:23 Changed 10 months ago by Richard Eisenberg <rae@…>

In 17bd1635/ghc:

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 10 months ago by RyanGlScott

Blocking: 14579 removed
Note: See TracTickets for help on using tickets.