CODEWITHSUNDEEP
haskelltype-inferencetypeclass
Sergey Kolbasov
Sergey Kolbasov

Reputation: 271

Typeclasses and type inference in Haskell

I'm trying to figure out how does type inference works together with type classes and so far struggle to grasp it fully.

Let's define the following simple HList:

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}

infixr 6 :::

data HList xs where
  HNil :: HList '[]
  (:::) :: a -> HList as -> HList (a ': as)

Now I'm going to define type class that allows to "uncurry" any function into the function of a single argument of type HList:

class FnToProduct fn ls out | fn ls -> out where
  fromFunction :: fn -> HList ls -> out

instance (FnToProduct' (IsArity1 fn) fn ls out) => FnToProduct fn ls out where
  fromFunction = fromFunction' @(IsArity1 fn)

class FnToProduct' (arity1 :: Bool) fn ls out | fn ls -> out where
  fromFunction' :: fn -> HList ls -> out

instance FnToProduct' True (input -> output) '[input] output where
  fromFunction' fn (a ::: tail) = fn a

instance (FnToProduct fnOutput tail out') => FnToProduct' False (input -> fnOutput) (input ': tail) out' where
  fromFunction' fn (input ::: tail) = fromFunction (fn input) tail

type family IsArity1 fn where
  IsArity1 (a -> b -> c) = False
  IsArity1 (a -> b) = True

Now I'm going to break the compilation:

test = fromFunction (\a b -> a) (True ::: False ::: HNil)

• Ambiguous type variables ‘p0’, ‘p1’,
                               ‘out0’ arising from a use of ‘fromFunction’
      prevents the constraint ‘(FnToProduct'
                                  'False (p1 -> p0 -> p1) '[Bool, Bool] out0)’ from being solved.
        (maybe you haven't applied a function to enough arguments?)
      Relevant bindings include test :: out0 (bound at src/HList.hs:98:1)
      Probable fix: use a type annotation to specify what ‘p0’, ‘p1’,
                                                          ‘out0’ should be.
      These potential instance exist:
        one instance involving out-of-scope types
        (use -fprint-potential-instances to see them all)
    • In the expression:
        fromFunction (\ a b -> a) (True ::: False ::: HNil)
      In an equation for ‘test’:
          test = fromFunction (\ a b -> a) (True ::: False ::: HNil)
   |
98 | test = fromFunction (\a b -> a) (True ::: False ::: HNil)
   |        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

But if I specify types of function explicitly:

test = fromFunction (\(a :: Bool (b :: Bool) -> a) (True ::: False ::: HNil)

It works just nice. How could I enforce type inference here so the compiler would pick up the types of HList to figure out types in function? I also tried to use infixl/r operators without any luck so far.

Upvotes: 2

Views: 661

Answers (2)

dfeuer
dfeuer

Reputation: 48580

Here's an option:

class (f ~ AbstractList ts o) => AppHList ts o f where
  appHList :: f -> HList ts -> o

type family AbstractList xs o where
  AbstractList '[] o = o
  AbstractList (x ': xs) o =
    x -> AbstractList xs o

instance f ~ o => AppHList '[] o f where
  appHList x HNil = x

instance (AppHList ts o f', f ~ (t -> f'))  => AppHList (t ': ts) o f where
  appHList f (x ::: xs) = appHList (f x) xs

Although there's only one equality constraint, this expresses dependencies in several directions. How's that? The key is that the type family can reduce as soon as the structure of the list is known; nothing is needed from the second argument and none of the list elements are needed either.

This seems to have the same inference power as HTNW's simplified version, but it has two advantages:

  1. It's possible to get equality evidence if you need it.
  2. It plays better with the PartialTypeSignatures extension. GHC seems to trip over the fundep version in that context for some reason. See this ticket I just filed.

But wait! There's more! This formulation suggests that even having a class is optional! The class-based approach is likely to be the most efficient when everything specializes and inlines completely, but this version looks a lot simpler:

appHList' :: f ~ AbstractList ts o => f -> HList ts -> o
appHList' x HNil = x
appHList' f (x ::: xs) = appHList' (f x) xs

Upvotes: 2

HTNW
HTNW

Reputation: 29148

Typeclasses are "matchy". In your example, GHC says it is trying to solve the constraint

FnToProduct' 'False (p1 -> p0 -> p1) '[Bool, Bool] out0

Where unification variables p1 and p0 coming from the implicit expansion of the first argument:

(\(a :: _p1) (b :: _p0) -> a)

and unification variable out0 coming from the type of fromFunction. Essentially, GHC doesn't know what the argument types should be, nor what the fromFunction call should eventually return, so it creates three variables to represent them and tries to figure out what they should be.

No instance matches this constraint. The

instance _ => FnToProduct' False (input -> fnOutput) (input ': tail) out'

would require p1 and Bool to be the same, but they aren't. They could be, as you demonstrate with your type-annotated example, but GHC believes that they don't have to be. You could imagine adding

instance _ => FnToProduct' False (Int -> fnOutput) (Bool ': tail) out'

and now you don't know whether a :: Int or a :: Bool, because both instances "fit". But, with the open world assumption, you have to assume new instances like this can be added whenever.

One fix is to use ~ constraints:

instance (i ~ i', o ~ o') => FnToProduct' True (i -> o) '[i'] o'
instance (i ~ i', FnToProduct r t o) => FnToProduct' False (i -> r) (i' ': t) o

The second instance now matches, because the two i variables are different. It actually guides type inference now, because the i ~ i' requirement, in this case, translates to a p1 ~ Bool requirement, which is used to instantiate p1. Similarly for p0, by the first instance.

Or, add another functional dependency. This doesn't always work, but it seems to do the job here

class FnToProduct fn ls out | fn ls -> out, fn out -> ls
class FnToProduct' (arity1 :: Bool) fn ls out | fn ls -> out, fn out -> ls

Which tells GHC that fs (and therefore its argument types, here p1 and p0) can be figure out from ls (here [Bool, Bool]).

That aside, I think your function could be simplified to this:

class AppHList ts o f | ts f -> o, ts o -> f where
   appHList :: f -> HList ts -> o
instance AppHList '[] o o where
   appHList x HNil = x
instance AppHList ts o f => AppHList (t : ts) o (t -> f) where
   appHList f (x ::: xs) = appHList (f x) xs

Artificially requiring the HList to supply all arguments is not particularly useful, and it can really blow up in polymorphic contexts, because you often can't tell what "supplying all the arguments" is supposed to mean. E.g. const can have any number of arguments, from 2 up. So, appHList const (id ::: 'a' ::: HNil) 6 works (where const has 3 arguments), but fromFunction fails in that context.

You can still impose the "returns a not-function" property externally to the more useful function, if you really want it.

type family IsFun f :: Bool where
  IsFun (_ -> _) = True
  IsFun _ = False
fullAppHList :: (IsFun o ~ False, AppHList ts o f) => f -> HList ts -> o
fullAppHList = appHList

Upvotes: 4

Related Questions