Hello, I have the following program: -------------------------------------------------------------------------- {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE ScopedTypeVariables #-} import Data.Proxy (Proxy) import Data.Typeable (Typeable, TypeRep, typeOf) data ProxyWrapper constraint = forall a. constraint a => ProxyWrapper (Proxy a) typeOfInnerProxy :: ProxyWrapper constraint -> TypeRep typeOfInnerProxy (ProxyWrapper p) = typeOfArg p typeOfArg :: forall t a. Typeable a => t a -> TypeRep typeOfArg _ = typeOf (undefined :: a) -------------------------------------------------------------------------- Type checking this gives the following expected type error: ProxyWrapper.hs:12:37: Could not deduce (Typeable a) arising from a use of `typeOfArg' from the context (constraint a) bound by a pattern with constructor ProxyWrapper :: forall (constraint :: * -> Constraint) a. (constraint a) => Proxy a -> ProxyWrapper constraint, in an equation for `typeOfInnerProxy' Is there a way to extend the 'constraint' with the 'Typeable' constraint in the type signature of 'typeOfInnerProxy'? Regards, Bas
Hi Bas. I haven't thought about this for long, but ...
data ProxyWrapper constraint = forall a. constraint a => ProxyWrapper (Proxy a)
I'm assuming adding Typable a in ProxyWrapper is not an option for you? So then what about: class (c1 a, c2 a) => Ext c1 c2 a instance (c1 a, c2 a) => Ext c1 c2 a typeOfInnerProxy :: ProxyWrapper (Ext Typeable constraint) -> TypeRep typeOfInnerProxy (ProxyWrapper p) = typeOfArg p This will certainly require all sorts of undecidable instances :) But does it work for you? Cheers, Andres -- Andres Löh, Haskell Consultant Well-Typed LLP, http://www.well-typed.com
On 5 June 2012 17:52, Andres Löh
Hi Bas.
I haven't thought about this for long, but ...
data ProxyWrapper constraint = forall a. constraint a => ProxyWrapper (Proxy a)
I'm assuming adding Typable a in ProxyWrapper is not an option for you?
No, I would rather keep that type as unconstrained as possible.
So then what about:
class (c1 a, c2 a) => Ext c1 c2 a instance (c1 a, c2 a) => Ext c1 c2 a
typeOfInnerProxy :: ProxyWrapper (Ext Typeable constraint) -> TypeRep typeOfInnerProxy (ProxyWrapper p) = typeOfArg p
This will certainly require all sorts of undecidable instances :) But does it work for you?
It works. Thanks a lot! Cheers, Bas
On 5 June 2012 17:57, Bas van Dijk
It works.
It turns out it doesn't work exactly as I want. Say I have this ProxyWrapper of Nums: p :: ProxyWrapper Num p = ProxyWrapper (Proxy :: Proxy Int) then the following would give a type error: oops :: TypeRep oops = typeOfInnerProxy p Couldn't match expected type `Ext Typeable constraint0' with actual type `Num' Expected type: ProxyWrapper (Ext Typeable constraint0) Actual type: ProxyWrapper Num In the first argument of `typeOfInnerProxy', namely `p' In the expression: typeOfInnerProxy p Bas
What you want seems a bit tricky.
p :: ProxyWrapper Num p = ProxyWrapper (Proxy :: Proxy Int)
At this point, all you know about p is that it is a Num. You don't know that it is Typeable, because you choose to forget about that. You could give p the type 'ProxyWrapper (Ext Typeable Num)' and it would work.
then the following would give a type error:
oops :: TypeRep oops = typeOfInnerProxy p
Yes, and correctly so. Because Typeable isn't even a superclass of Num. So there's no way to know that p actually contains a Typeable proxy. Cheers, Andres -- Andres Löh, Haskell Consultant Well-Typed LLP, http://www.well-typed.com
On Tue, Jun 5, 2012 at 5:29 PM, Bas van Dijk
Hello,
I have the following program:
-------------------------------------------------------------------------- {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE ScopedTypeVariables #-}
import Data.Proxy (Proxy) import Data.Typeable (Typeable, TypeRep, typeOf)
data ProxyWrapper constraint = forall a. constraint a => ProxyWrapper (Proxy a)
I must be missing something, but this seems a bit useless to me. You have a phantom type parameter on Proxy, and then you're hiding it. So when you pattern match on ProxyWrapper you recover the fact that there was a type which satisfies the constraint, but you don't know what type it was, and neither do you know about any values which are of the type. What are you trying to do? That said, if you want to be able to recover a Typeable constraint, I don't see any way except for using 'ProxyWrapper (Ext Typeable constraint)' as Andres says or putting 'forall a. (constraint a, Typeable a)' in the definition of ProxyWrapper.
typeOfInnerProxy :: ProxyWrapper constraint -> TypeRep typeOfInnerProxy (ProxyWrapper p) = typeOfArg p
typeOfArg :: forall t a. Typeable a => t a -> TypeRep typeOfArg _ = typeOf (undefined :: a) --------------------------------------------------------------------------
Type checking this gives the following expected type error:
ProxyWrapper.hs:12:37: Could not deduce (Typeable a) arising from a use of `typeOfArg' from the context (constraint a) bound by a pattern with constructor ProxyWrapper :: forall (constraint :: * -> Constraint) a. (constraint a) => Proxy a -> ProxyWrapper constraint, in an equation for `typeOfInnerProxy'
Is there a way to extend the 'constraint' with the 'Typeable' constraint in the type signature of 'typeOfInnerProxy'?
Regards,
Bas
On 5 June 2012 18:46, Gábor Lehel
I must be missing something, but this seems a bit useless to me. You have a phantom type parameter on Proxy, and then you're hiding it. So when you pattern match on ProxyWrapper you recover the fact that there was a type which satisfies the constraint, but you don't know what type it was, and neither do you know about any values which are of the type. What are you trying to do?
I need a list of types that satisfy a certain constraint. I would like to have the static guarantee that types that don't satisfy the constraint can't be put in the list, as in: nums :: [ProxyWrapper Num] nums = [ ProxyWrapper (Proxy :: Proxy Int) , ProxyWrapper (Proxy :: Proxy Double) , ProxyWrapper (Proxy :: Proxy String) -- not allowed ] fracs :: [ProxyWrapper Fractional] fracs = [ ProxyWrapper (Proxy :: Proxy Double) , ProxyWrapper (Proxy :: Proxy Float) , ProxyWrapper (Proxy :: Proxy Int) -- not allowed ]
That said, if you want to be able to recover a Typeable constraint, I don't see any way except for using 'ProxyWrapper (Ext Typeable constraint)' as Andres says or putting 'forall a. (constraint a, Typeable a)' in the definition of ProxyWrapper.
Indeed, I'm now going for the latter option. Regards, Bas
participants (3)
-
Andres Löh -
Bas van Dijk -
Gábor Lehel