Opened 11 months ago

Last modified 11 months ago

#15782 new feature request

Visible type/kind applications in declaration of data/type constructors

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

Description (last modified by Iceland_jack)

I'm making this ticket to keep track of this, I don't know if it's a good idea.

Allow visible type/kind applications when declaring data/type constructors on the LHS of :: (from Phab comment).

data
    Proxy @k :: k -> Type where
  MkProxy @k :: Proxy @k (a :: k)

&

data
  Fin     :: N -> Type where
  FinO @n ::          Fin (S n)
  FinS @n :: Fin n -> Fin (S n)

&

data
  Elem  @k @n  :: Vec n k -> Type where
  ElemO @a @as :: Elem @k @(S n) (a:>as)
  ElemS @a @as :: Elem @k @n     as
               -> Elem @k @(S n) (a:>as)

Change History (4)

comment:1 Changed 11 months ago by Iceland_jack

Description: modified (diff)

comment:2 Changed 11 months ago by Iceland_jack

Description: modified (diff)

comment:3 Changed 11 months ago by Iceland_jack

Consider also, declarations of type classes and synonyms

class    (f a, g a) => (&) @k f g a
instance (f a, g a) => (&) @k f g a -- on the VKA branch, only this works
type Cat ob = ob -> ob -> Type

class Category (ob :: Type) where
 type Hom @ob :: Cat ob

 id  :: Hom @ob a a
 (.) :: Hom @ob b c -> Hom @ob a b -> Hom @ob a c

Now for an extreme example, but what about this

class Category @ob where
  type Hom @ob :: Cat ob
  id :: Hom @ob a a

where the type of id is id :: forall (a :: ob). Category @ob => Hom a a.

comment:4 Changed 11 months ago by goldfire

I generally support this. But this has to go via a proposal, not just a ticket.

Note: See TracTickets for help on using tickets.