Can I get 'forall (a :: k). Typeable a => Dict (Typeable k)'?

Morally I think that class Typeable (a :: k) should have been class Typeable k => Typeable (a :: k) If I'm wrong, could someone please elaborate why? If I'm right, please read on ... That would be a breaking change, but could we at least get kindable :: forall (a :: k). Typeable a => Dict (Typable (a :: k)) in the meantime? Tom

On rereading maybe my question is a big ambiguous. What I'm really asking is "do people support the addition of (and see the value of) a function of the following type?" forall (a :: k). Typeable a => Dict (Typable (a :: k)) It might require changes to GHC, I'm not sure. I suppose the new/proposed ghc-experimental package would be a good place for it to start its life. Tom On Wed, Aug 23, 2023 at 11:50:10AM +0100, Tom Ellis wrote:
Morally I think that
class Typeable (a :: k)
should have been
class Typeable k => Typeable (a :: k)
If I'm wrong, could someone please elaborate why? If I'm right, please read on ...
That would be a breaking change, but could we at least get
kindable :: forall (a :: k). Typeable a => Dict (Typable (a :: k))
in the meantime?

As I answered in my other mail: no. There is Type.Reflection.typeRep, which does that. Also Dict is not in base, you'd first need to add that there. - Oleg On 23.8.2023 13.54, Tom Ellis wrote:
On rereading maybe my question is a big ambiguous. What I'm really asking is "do people support the addition of (and see the value of) a function of the following type?"
forall (a :: k). Typeable a => Dict (Typable (a :: k))
It might require changes to GHC, I'm not sure. I suppose the new/proposed ghc-experimental package would be a good place for it to start its life.
Tom
On Wed, Aug 23, 2023 at 11:50:10AM +0100, Tom Ellis wrote:
Morally I think that
class Typeable (a :: k)
should have been
class Typeable k => Typeable (a :: k)
If I'm wrong, could someone please elaborate why? If I'm right, please read on ...
That would be a breaking change, but could we at least get
kindable :: forall (a :: k). Typeable a => Dict (Typable (a :: k))
in the meantime?
Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

What you mean "could we get", add to base or be able to define? I think you can: {-# LANGUAGE GADTs, RankNTypes, KindSignatures, PolyKinds, ConstraintKinds #-} import Data.Kind import Type.Reflection data Dict (c :: Constraint) where Dict :: c => Dict c kindable :: forall {k} (a :: k). Typeable a => Dict (Typeable (a :: k)) kindable = Dict works? Or am I missing something? Also isn't TypeRep a from Type.Reflection the same as Dict (Typeable a) for all practical purposes, `kindable = Type.Reflection.typeRep`, yet better? kindable' :: forall {k} (a :: k). Typeable a => TypeRep a kindable' = typeRep - Oleg On 23.8.2023 13.50, Tom Ellis wrote:
Morally I think that
class Typeable (a :: k)
should have been
class Typeable k => Typeable (a :: k)
If I'm wrong, could someone please elaborate why? If I'm right, please read on ...
That would be a breaking change, but could we at least get
kindable :: forall (a :: k). Typeable a => Dict (Typable (a :: k))
in the meantime?
Tom _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

No, sorry, it's me who's missing something. The subject line of my email is correct, but the content was not. What I wanted was a way of writing forall (a :: k). Typeable a => Dict (Typeable k) or, if you like forall (a :: k). Typeable a => TypeRep k Given your suggestion I searched for usages of TypeRep in the documentation and found that (something equivalent to) it already exists: typeRepKind :: TypeRep (a :: k) -> TypeRep k https://www.stackage.org/haddock/lts-21.8/base-4.17.2.0/Type-Reflection.html... So problem solved. Thanks! Tom On Wed, Aug 23, 2023 at 01:58:16PM +0300, Oleg Grenrus wrote:
I missing something?
On 23.8.2023 13.50, Tom Ellis wrote:
Morally I think that
class Typeable (a :: k)
should have been
class Typeable k => Typeable (a :: k)
If I'm wrong, could someone please elaborate why? If I'm right, please read on ...
That would be a breaking change, but could we at least get
kindable :: forall (a :: k). Typeable a => Dict (Typable (a :: k))
in the meantime?

Hi Tom, I think you are looking for Type.Reflection.typeRepKind typeRepKind :: TypeRep (a :: k) -> TypeRep k which combined with typeRep :: Typeable a => TypeRep a withTypeable :: forall k (a :: k) rep (r :: TYPE rep). TypeRep a -> (Typeable a => r) -> r should allow you to define kindable :: forall (a :: k). Typeable a => Dict (Typeable k) as your subject line asked for, albeit not the message body. :-) Cheers, Adam On 23/08/2023 11:50, Tom Ellis wrote:
Morally I think that
class Typeable (a :: k)
should have been
class Typeable k => Typeable (a :: k)
If I'm wrong, could someone please elaborate why? If I'm right, please read on ...
That would be a breaking change, but could we at least get
kindable :: forall (a :: k). Typeable a => Dict (Typable (a :: k))
in the meantime?
Tom
-- Adam Gundry, Haskell Consultant Well-Typed LLP, https://www.well-typed.com/ Registered in England & Wales, OC335890 27 Old Gloucester Street, London WC1N 3AX, England

On Wed, Aug 23, 2023 at 12:10:24PM +0100, Adam Gundry wrote:
I think you are looking for Type.Reflection.typeRepKind
typeRepKind :: TypeRep (a :: k) -> TypeRep k [...] as your subject line asked for, albeit not the message body. :-)
Yes, exactly, thank you! Tom
participants (3)
-
Adam Gundry
-
Oleg Grenrus
-
Tom Ellis