Hi again, On 6/8/07, Emilio Jesús Gallego Arias wrote:

I guess this is due to types like

...

type A a = Show a => a type B a = Show a => a

You're right. This is not valid in the standard nor GHC.

so if you do

...

f :: A a -> B b it should get translated to f :: (Show a => a) -> (Show b => b)

Which is not valid. I wonder if regrouping all the contexts in the left side should work:

...

f :: (Show a, Show b) => a -> b

Maybe it can be feasible to implement that behavior, but it clearly doesn't work like that right now. Maybe some GHC guru reading this could explain why? You can get the effect you want by using existentials to pack the constraint with the type type Discard a = forall b. Show b => a -> b -> (a, String) thus, a function f :: Discard a -> Discard b would expand to something like f :: (forall b. Show b => a -> b -> (a, String)) -> (forall c. Show c => b -> c -> (c, String))

...

In addition you seem to be trying to pack a dictionary with the type (something you cannot do in Haskell without existentials). This is

Why? My first guess it that there's no way to translate that to system F, but if we look at 'type' as a macro, it could make sense.

No idea, but that's how it works (I've been hitting myself against the wall to solve similar problems and existentials seem the only way to go).

...

just a guess, but it seems that a definition using existentials is what you're looking for.

data FSet a = forall a. Show a => FSet (a -> Double)

That would be

...

data FSet = forall a. Show a => FSet (a -> Double)

not?

Yep, you're right. a is alredy universally quantified in the RHS. This is probably what you're looking for: type FSet a = forall a. Show a => FSet (a -> Double)

I'm not looking yet for existential types, as then my functions will have to hold for every a, which turns out to be very inconvenient.

hold?

The reason I don't want to use data, which works ok, is because I'd like to use FSet as a function, but not to write the type constraint in every function using as it is now.

I know, it can be a pain to have to carry the type class constraints everywhere. Maybe the type redefinition using existentials I wrote above can help. Otherwise I guess you'll have to cope with writting the constraint in every function signature.

Hi Alfonso! "Alfonso Acosta" writes:

On 6/8/07, Emilio Jesús Gallego Arias wrote:

Yep, you're right. a is alredy universally quantified in the RHS. This is probably what you're looking for:

type FSet a = forall a. Show a => (a -> Double)

...

I'm not looking yet for existential types, as then my functions will have to hold for every a, which turns out to be very inconvenient.

hold?

See,

type FSet = forall a . Show a => (a -> Double)

up :: Double -> Double up x = x + 1

m :: FSet m = up

This doesn't work. I really want to use some functions that are not general enough. If the function cannot touch it's value (as it's the case with forall), then the function is almost useless, unless you'd like to do some type level programming. I'd like to have different functions for the same type, so I cannot pack it into a type class.

...

The reason I don't want to use data, which works ok, is because I'd like to use FSet as a function, but not to write the type constraint in every function using as it is now.

I know, it can be a pain to have to carry the type class constraints everywhere. Maybe the type redefinition using existentials I wrote above can help. Otherwise I guess you'll have to cope with writting the constraint in every function signature.

Yeah, in general Haskell types don't carry constraints, however, I don't see the reason that this doesn't work when using type level macros, as

type F a = C a => a

should just be a macro and substitute. Regards, Emilio