Can I select an instance without resorting to TypeApplications?

user_2289983 0
Viewed 128

I have the following type classes:

{-# LANGUAGE AllowAmbiguousTypes    #-}
{-# LANGUAGE InstanceSigs           #-}
{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE MultiParamTypeClasses  #-}

class Interpretation i where
  type Context i :: * -> *

class Interpretation i => Interpret i a where
  type Interpreted i a :: *

  int :: a -> Context i (Interpreted i a)

Which basically encode interpretation functions from a to Interpreted i a wrapped in some context.

I've written these instances:

data X = X

instance Interpretation X where
  type Context X = Identity

instance Interpret X Int where
  type Interpreted X Int = Bool

  int :: Int -> Identity Bool
  int x = pure (x == 0)

Now suppose that I need to use int above to interpret an Int into a Bool, for instance in the following function:

f :: Int -> Bool
f = -- use int somehow

If I define f as follows:

f x = int x

The compiler will complain:

• Couldn't match type ‘Interpreted i0 Int’ with ‘Bool’
  Expected type: Int -> Identity Bool
    Actual type: Int -> Context i0 (Interpreted i0 Int)
  The type variable ‘i0’ is ambiguous
• In the second argument of ‘(.)’, namely ‘int’
  In the expression: runIdentity . int
  In an equation for ‘f’: f = runIdentity . int

By using TypeApplications I can select the right (and only available) instance:

{-# LANGUAGE TypeApplications       #-}

-- ...

f :: Int -> Bool
f = runIdentity . int @X

But I was wondering whether such instance could be selected without resorting to TypeApplications.

type-families haskell
2 Answers

No. Imagine, if we had in another module

instance Interpretation Y where
  type Context Y = Identity

instance Interpret Y Int where
  type Interpreted Y Int = Bool

  int :: Int -> Identity Bool
  int x = pure (x /= 0)

And define f as you have done - what should the behaviour be?

I assume you also don't want to use something like Proxy, which would allow you to pass in a type variable without needing to use TypeApplications, but would still require specifying the instance you'd want to use.

user_59472470

As it stands, int has an ambiguous type. That's because i only appears in the signature within Context i and Interpreted i a, which are type families and as such not (necessarily) injective, as witnessed by Isaac van Bakel's answer. Ambiguous types can only be resolved with type applications (and IMO this is a perfectly good approach).

You can however prevent the ambiguity. The traditional way is to use associated data families instead of type families; these have the type information baked in and are therefore always injective:

class Interpretation i where
  data Context i a

class Interpretation i => Interpret i a where
  type Interpreted i a :: *
  int :: a -> Context i (Interpreted i a)

instance Interpretation X where
  newtype Context X a = XContext (Identity a)

instance Interpret X Int where
  type Interpreted X Int = Bool
  int :: Int -> Context X Bool
  int x = XContext $ pure (x == 0)

f :: Int -> Bool
f n = case int n of
  XContext a -> runIdentity a

An alternative is the more recent injective type families extension.

{-# LANGUAGE TypeFamilyDependencies #-}

class Interpretation i where
  type Context i = (r :: * -> *) | r -> i

class Interpretation i => Interpret i a where
  type Interpreted i a :: *
  int :: a -> Context i (Interpreted i a)

instance Interpretation X where
  type Context X = Identity

instance Interpret X Int where
  type Interpreted X Int = Bool
  int :: Int -> Identity Bool
  int x = pure (x == 0)

f :: Int -> Bool
f = runIdentity . int

Note that in this case, you won't be able to use Identity for another Interpretation instance.

user_7459030
Related