CODEWITHSUNDEEP
haskellfoldtype-level-computation
Jon Purdy
Jon Purdy

Reputation: 55029

Polymorphic functions over chains of nested tuples

Suppose I have a list of types, of kind [*]:

let Ts = '[Int, Bool, Char]

I want to convert this to a chain of tuples:

type family Tupled (ts :: [*]) z :: *
type instance Tupled (t ': ts) z = (t, Tupled ts z)
type instance Tupled '[] z = z

So far so good:

> :kind! Tupled Ts ()
Tupled Ts () :: *
= (Int, (Bool, (Char, ())))

Now I’d like to be able to write a type Fun to represent functions that are polymorphic in the “bottom” of this chain. For example, Fun Ts Ts should work on either of these types:

(Int, (Bool, (Char, (String, ()))))
(Int, (Bool, (Char, (Word, (ByteString, ())))))

I tried this:

newtype Fun as bs = Fun
  { unfun :: forall z. Tupled as z -> Tupled bs z }

But it fails to typecheck:

Couldn't match type ‘Tupled bs z’ with ‘Tupled bs z0’
NB: ‘Tupled’ is a type function, and may not be injective
The type variable ‘z0’ is ambiguous
Expected type: Tupled as z -> Tupled bs z
  Actual type: Tupled as z0 -> Tupled bs z0
In the ambiguity check for the type of the constructor ‘Fun’:
  Fun :: forall z. Tupled as z -> Tupled bs z
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the definition of data constructor ‘Fun’
In the newtype declaration for ‘Fun’

I’ve seen recommendations to use a data family to avoid problems with injectivity:

data family Tupled (ts :: [*]) z :: *
data instance Tupled (t ': ts) z = Cons t (Tupled ts z)
data instance Tupled '[] z = Nil

And indeed that makes Fun compile, but it looks like that gets me “stuck” in the land of Cons and Nil when I’m looking to work with tuples, like this:

Fun $ \ (i, (b, (c, z))) -> (succ i, (not b, (pred c, z)))

Can I work around this somehow?

Upvotes: 5

Views: 186

Answers (1)

András Kovács
András Kovács

Reputation: 30103

Enable AllowAmbiguousTypes. From GHC 8, the ambiguity check is completely superfluous, because any (fundamentally resolvable) ambiguity can be resolved with type applications. Also, your case seems to be just a false positive for ambiguity check, since we can clearly use Fun even without type applications.

Upvotes: 4

Related Questions