Is there a way to use type variables bound outside a function’s type declaration?

Learn
#1

Let’s say I have a couple of functions like this:

f :: forall t. Foo (t -> Bar Integer) => t -> Integer
g :: forall t. Foo (t -> Bar ()) => t -> Integer

and their definitions use TypeApplications and ScopedTypeVariables to declare the Foo instance to use, since it’s ambiguous. I cannot write a type synonym Fubar…

type Fubar i = forall t. Foo (t -> Bar i) => t -> Integer

…since this will no longer bind t in the type declarations.

Can I somehow extract or bubble up the t variable? Could a type synonym have an additional output channel that can be bound?

#2

I think you want the following, don’t you?

type Fubar i t = Foo (t -> Bar i) => t -> Integer

That said, I don’t understand why there would be any ambiguity there. Could you paste a complete Haskell program that demonstrates the problem?

#3

So there’s no way to do it while including forall inside the type synonym?

#4

I don’t know because I don’t really understand why you are trying to do this. Could you elaborate a little, perhaps pasting a complete example of what you really want to achieve?

#5

Honestly, just to save space, since forall could be repeated very often.

There’s no real good reason for this.

#6

I’ve also tried to figure this out for some time. My motivation was the use in backpack signatures where it is even more important to be able to do this. For example take the signature which is like the Semigroup class:

type A
append :: A -> A -> A

This signature cannot be instantiated by polymorphic lists because you would need to write:

type A = [a] -- where is 'a' bound?
append = (++)

But that fails to compile.

The only workaround I could come up with is using type classes with equality constraints as superclasses. Here’s what I mean:

class A a where
  append :: a -> a -> a

Which can be instantiated by the module:

class A a where
  append :: a -> a -> a
instance a ~ [b] => A a where
  append = (++)

You might ask why even use backpack modules at all at this point, because the existing Semigroup class is already very similar. The advantage of this approach is that the A constraint is guaranteed to be resolved at compile time, so it will never be translated to dictionary passing. The disadvantage is that it now is specialized to a single type (the type of lists).

So, I would really also like a nicer way to float out type variables.

#7

Honestly, just to save space

Seems reasonable! I still don’t understand the problem though. What goes wrong if you rewrite f to

#8

It’s not using a type synonym.

Basically I just wanted to confirm the type synonym irrevocably hides the quantification.

1 Like