Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Overlapping instances to flatten tuples

I'm trying to write code to remove empty tuples from a tuple chain. The compiler rejects the program:

Code:

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverlappingInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeOperators #-}

infixr 9 :*
data a :* b = a :* !b
  deriving (Show, Eq, Ord)

class Flatten a b | a -> b where
  flatten :: a -> b

instance Flatten a a where
  flatten = id

instance Flatten a b => Flatten (() :* a) b where
  flatten (() :* y) = flatten y

instance Flatten b c => Flatten (a :* b) (a :* c) where
  flatten (x :* y) = x :* flatten y


test :: Int :* ()
test = flatten $ 0 :* ()

[1 of 1] Compiling Main             ( Test\Test.hs, interpreted )

Test\Test.hs:26:8:
    Overlapping instances for Flatten (Int :* ()) (Int :* ())
      arising from a use of `flatten'
    Matching instances:
      instance [overlap ok] Flatten a a
        -- Defined at Test\Test.hs:15:10-20
      instance [overlap ok] Flatten b c => Flatten (a :* b) (a :* c)
        -- Defined at Test\Test.hs:21:10-49
    In the expression: flatten
    In the expression: flatten $ 0 :* ()
    In an equation for `test': test = flatten $ 0 :* ()
Failed, modules loaded: none.

Goal:

flatten (0:*():*1:*2:3:*():*():*4:*()) == (0:*1:*2:*3:*4:*())
like image 668
Thomas Eding Avatar asked Dec 27 '22 08:12

Thomas Eding


1 Answers

Okay, first of all: The reason the compiler complains about the fundeps conflicting is... because they do conflict. There's really no way around that, as such--the conflict is inherent in what you're trying to do. The first type parameter is the "input", and you're essentially pattern matching on it for specific types, with overlapping giving default fall-through cases. But the second, "output" type parameter needs to vary depending on the "input" in ways that differ between the specific and default cases, thus the conflict.

To work around this, you need to employ a bit of trickery exploiting the fact that GHC examines only the instance head when choosing an instance, then checks the context later to apply additional constraints. The core of the trick is to leave the "output" type completely unspecified, so that instance selection examines only the first parameter and thinks the second is identical for all instances, while slipping something into the context that unifies the second parameter with the desired "output" after the fact.

The easiest way to use this technique in current GHC versions is to enable type families as well to get the ~ equality constraint feature. Here's an example:

instance (() ~ r) => Flatten (() :* ()) r where
  flatten _ = ()

instance (Flatten a r) => Flatten (() :* a) r where
  flatten (_ :* rest) = flatten rest

instance (a ~ r) => Flatten (a :* ()) r where
  flatten (x :* _) = x

instance ((a :* c) ~ r, Flatten b c) => Flatten (a :* b) r where
  flatten (x :* rest) = (x :* flatten rest)

instance (a ~ r) => Flatten a r where
  flatten x = x

To illustrate the pattern I've made every instance use this trick, even when not absolutely necessary. We can define the input you want:

test = (0 :* () :* 1 :* 2 :* 3 :* () :* () :*4 :* ()) 

And then, in GHCi:

∀x. x ⊢ flatten test
0 :* (1 :* (2 :* (3 :* 4)))

Now, you may be wondering why I defined test outside of GHCi. Unfortunately, the above instances will still fail if applied to a polymorphic input type, and loading it from a file causes the monomorphism restriction and type defaulting to turn all the numeric literals into Integer. There's really not much that can be done about such ambiguity, though, because a type parameter that could match multiple inputs is, indeed, ambiguous.


As a historical note, you can do the same trick without ~, using only fundeps and weird quirks of GHC. Some version of this is required for a great deal of ridiculous type hackery, and the original was (unsurprisingly) invented by Oleg, going by the slightly misleading name TypeCast, and was used to implement the equality predicate TypeEq which underlies things like HList.

like image 184
C. A. McCann Avatar answered Jan 07 '23 16:01

C. A. McCann