[GHC] #11620: RFC: Type-class type signatures (:: Constraint)
#11620: RFC: Type-class type signatures (:: Constraint) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature | Status: new request | Priority: normal | Milestone: Component: Compiler | Version: 8.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Data types can be defined: {{{#!hs data A a b -- or data A (a :: Bool) (b :: Type) -- or data A (a :: Bool) (b :: Type) :: Type -- or data A :: Bool -> Type -> Type data B :: Type }}} while type classes can't: {{{#!hs class A a b -- or class A (a :: Bool) (b :: Type) -- but not -- class A (a :: Bool) (b :: Type) :: Constraint -- nor -- class A :: Bool -> Type -> Constraint -- class B :: Constraint }}} I foresee problems with how to bind `a` and `b`, but adding a final `:: Constraint` should be legal: {{{#!hs class A a b :: Constraint class A (a :: Bool) (b :: Type) :: Constraint class B :: Constraint }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11620 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11620: RFC: Type-class type signatures (:: Constraint) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: 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): I actually ran into this problem in a different context, where the problem was not just cosmetic. Short version: we should devise a syntax where a user can give a full kind signature for a class while binding type variables appropriately. I'm not sure what this syntax would be. Long version: I had this type: {{{#!hs data TypeRep (a :: k) where ... }}} I needed an existential wrapper around this type, something like {{{#!hs data TypeRepX1 where TypeRepX1 :: forall k (a :: k). TypeRep a -> TypeRepX1 }}} But that turned out not to work for me, because it imposes no constraint at all on `k` or `a`. So I wanted a version of `TypeRepX` that is parameterized by a constraint that will be applied to `a`. If the existential `a` is still to be kind-polymorphic, then we have to make the constraint kind-polymorphic, too: {{{#!hs data TypeRepX :: (forall k. k -> Constraint) -> Type where TypeRepX :: forall (c :: forall k1. k1 -> Constraint) k (a :: k). c a => TypeRep a -> TypeRepX c }}} (Sadly, I need to put the kind on `c` explicitly, because GHC won't infer kinds with `forall`s, lest things become impredicative. But it's not so bad, really, to put the signature on.) This actually all works quite well, to my great delight when I first tried it. Then, I wanted to use the constraint `((~~) Bool)`. That is, I wanted to insist that the type `a` is in fact `Bool`. I used heterogeneous equality so that it would all be kind-polymorphic. However, note that {{{#!hs (~~) :: forall k1 k2. k1 -> k2 -> Constraint` }}} and thus that {{{#!hs (~~) Bool :: k2 -> Constraint }}} for some `k2`. That is, the original `forall` is too far to the left. As you will see in the "Practical type inference" paper, the kind of `(~~)` is too specific; it should really be `forall k1. k1 -> forall k2. k2 -> Constraint`. But we have no way of requesting such a kind without being able to specify the full kind signature of a class. (In the case of `(~~)`, GHC could just do this by fiat. But it would be unsporting for me to do this for `(~~)` without letting you do it for your constraints.) Bottom line: it would increase the expressiveness of Haskell to be able to specify a full kind. But what about syntax?? I'm a bit stuck there. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11620#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11620: RFC: Type-class type signatures (:: Constraint) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: 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): Thanks for the response, interesting. {{{#!hs -- Dependent function syntax class HRefl :: forall k1. (a::k1) -> forall k2. (b::k2) -> Constraint -- Specify variables separately, as in functions and `type families' -- foo :: forall a. [a] -> forall b. [b] -> Int -- foo xs ys = length xs + length ys class HEq :: forall k1. k1 -> forall k2. k2 -> Constraint HEq a b }}} Is there an effort to unify all these forms (not only syntactically); functions, type families, type classes, GADTs? Just for fun {{{#!hs data Vec Nat Type :: Type Vec n a data Vec :: Nat -> Type -> Type Vec n a class Eq :: forall k. k -> k -> Constraint Eq a b where HEq @k a @k b a implies b b implies a }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11620#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC