Calculating Arity

Posted on by Chris Warburton

The arity of a value is the number of arguments it can accept. We can define arity by pattern-matching on types (a feature known as typecase):

arity (I -> O) = 1 + arity O
arity  T       = 0

However, it's difficult to implement this kind of type-level function. Here are some approaches I tried in Haskell.

Type Classes

We want arity to have a different value, depending on the type we're using. We can do this by overloading arity using type classes:

class HasArity a where
  arity :: Int

However, we hit problems if we try to implement this type class:

instance (HasArity o) => HasArity (i -> o) where
  arity = 1 + arity

instance HasArity t where
  arity = 0

There are two issues here. Firstly, we don't know which arity to use in the expression 1 + arity:


/tmp/nix-build-blog-2015-11-12-calculating_arity.html.drv-0/runghcXXXX1804289383846930886.hs:2:3: error:
    • Could not deduce (HasArity a0)
      from the context: HasArity a
        bound by the type signature for:
                   arity :: HasArity a => Int
        at /tmp/nix-build-blog-2015-11-12-calculating_arity.html.drv-0/runghcXXXX1804289383846930886.hs:2:3-14
      The type variable ‘a0’ is ambiguous
    • In the ambiguity check for ‘arity’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      When checking the class method:
        arity :: forall a. HasArity a => Int
      In the class declaration for ‘HasArity’

We can fix this by turning arity into a function:

class HasArity a where
  arity :: a -> Int

instance (HasArity o) => HasArity (i -> o) where
  -- undefined inhabits every type, including i
  arity f = 1 + arity (f undefined)

instance HasArity t where
  arity _ = 0

The other problem is that these two instances overlap; the first is just a special case of the second:

main = print (arity not)

/tmp/nix-build-blog-2015-11-12-calculating_arity.html.drv-0/runghcXXXX1804289383846930886.hs:10:15: error:
    • Overlapping instances for HasArity (Bool -> Bool)
        arising from a use of ‘arity’
      Matching instances:
        instance HasArity t
          -- Defined at /tmp/nix-build-blog-2015-11-12-calculating_arity.html.drv-0/runghcXXXX1804289383846930886.hs:8:10
        instance HasArity o => HasArity (i -> o)
          -- Defined at /tmp/nix-build-blog-2015-11-12-calculating_arity.html.drv-0/runghcXXXX1804289383846930886.hs:4:10
    • In the first argument of ‘print’, namely ‘(arity not)’
      In the expression: print (arity not)
      In an equation for ‘main’: main = print (arity not)

Unlike pattern-matching, which tries alternatives from top to bottom, type classes don't have such an ordering. This makes it difficult to implement a "catch-all" instance which works for any type other than functions.

Multi-Parameter Type Classes

The classic way to implement type-level computation in Haskell is to use multi-parameter type classes as a form of logic programming. Similar to Prolog, to represent a total function of the form arity x = a, we instead define a partial relation of the form arity x a. We can then implement that relation as a multi-parameter type class, relating the input type to its arity:

class HasArity a n where
  arity :: a -> n

Unfortunately, Haskell doesn't have dependent types, so we can't represent arities with regular numbers:

instance (HasArity o n) => HasArity (i -> o) (1 + n) where
  arity f = 1 + arity (f undefined)

instance HasArity t 0 where
  arity _ = 0

/tmp/nix-build-blog-2015-11-12-calculating_arity.html.drv-0/runghcXXXX1804289383846930886.hs:3:47: error:
    Illegal type: ‘1’ Perhaps you intended to use DataKinds

/tmp/nix-build-blog-2015-11-12-calculating_arity.html.drv-0/runghcXXXX1804289383846930886.hs:3:47: error:
    Not in scope: type constructor or class ‘+’

/tmp/nix-build-blog-2015-11-12-calculating_arity.html.drv-0/runghcXXXX1804289383846930886.hs:3:47: error:
    Illegal operator ‘+’ in type ‘1 + n’
      Use TypeOperators to allow operators in types

/tmp/nix-build-blog-2015-11-12-calculating_arity.html.drv-0/runghcXXXX1804289383846930886.hs:6:21: error:
    Illegal type: ‘0’ Perhaps you intended to use DataKinds

Type-level programming in Haskell can only involve types, not regular values like numbers, so we need some type-level notion of numbers instead. In other words, an arity n is both a type and a number; it's not a "numeric type", like Int, since Int itself is not a number; likewise it's not an element of a numeric type like Int, like 3 :: Int, since Ints are not types. We need a new notion, which satisfies both of these requirements:

-- Type level Peano numerals
data Zero   = Z
data Succ n = S n

To make life easier, we provide a toInt function to turn these Peano numbers into regular Ints:

class ToInt a where
  toInt :: a -> Int

instance ToInt Zero where
  toInt _ = 0

instance (ToInt n) => ToInt (Succ n) where
  toInt (S x) = 1 + toInt x

Now we can return these Peano numbers from our arity functions:

instance (HasArity o n) => HasArity (i -> o) (Succ n) where
  arity f = S (arity (f undefined))

instance HasArity t Zero where
  arity _ = Z

This gets us part of the way there; our arities are now living at the same level as our types, but now we have a couple of problems regarding ambiguity:

main = print (arity not)

/tmp/nix-build-blog-2015-11-12-calculating_arity.html.drv-0/runghcXXXX1804289383846930886.hs:19:8: error:
    • Ambiguous type variable ‘a0’ arising from a use of ‘print’
      prevents the constraint ‘(Show a0)’ from being solved.
      Probable fix: use a type annotation to specify what ‘a0’ should be.
      These potential instances exist:
        instance Show Ordering -- Defined in ‘GHC.Show’
        instance Show Integer -- Defined in ‘GHC.Show’
        instance Show a => Show (Maybe a) -- Defined in ‘GHC.Show’
        ...plus 22 others
        ...plus 11 instances involving out-of-scope types
        (use -fprint-potential-instances to see them all)
    • In the expression: print (arity not)
      In an equation for ‘main’: main = print (arity not)

/tmp/nix-build-blog-2015-11-12-calculating_arity.html.drv-0/runghcXXXX1804289383846930886.hs:19:15: error:
    • Ambiguous type variable ‘a0’ arising from a use of ‘arity’
      prevents the constraint ‘(HasArity
                                  (Bool -> Bool) a0)’ from being solved.
        (maybe you haven't applied a function to enough arguments?)
      Probable fix: use a type annotation to specify what ‘a0’ should be.
      These potential instances exist:
        instance HasArity t Zero
          -- Defined at /tmp/nix-build-blog-2015-11-12-calculating_arity.html.drv-0/runghcXXXX1804289383846930886.hs:17:10
        instance HasArity o n => HasArity (i -> o) (Succ n)
          -- Defined at /tmp/nix-build-blog-2015-11-12-calculating_arity.html.drv-0/runghcXXXX1804289383846930886.hs:14:10
    • In the first argument of ‘print’, namely ‘(arity not)’
      In the expression: print (arity not)
      In an equation for ‘main’: main = print (arity not)

Functional Dependencies

These ambiguities are due to the open nature of type classes: we can declare new instances at any point, so the fact that we just-so-happen to have instances with Zero and Succ n as the second parameter doesn't actually tell Haskell very much; it might come across other definitions elsewhere which use other types as the second parameter, and hence there is ambiguity.

To make the second parameter unambiguous we can use functional dependencies to indicate that the second parameter is completely determined by the first one:

class HasArity a n | a -> n where
  arity :: a -> n

Now we can make our two instances:

instance (HasArity o n) => HasArity (i -> o) (Succ n) where
  arity f = S (arity (f undefined))

instance HasArity t Zero where
  arity _ = Z

However, we still have an ambiguity problem; the "catch-all" parameter t of the second instance overlaps with the more-specific function type i -> o of the first:


/tmp/nix-build-blog-2015-11-12-calculating_arity.html.drv-0/runghcXXXX1804289383846930886.hs:14:10: error:
    Functional dependencies conflict between instance declarations:
      instance HasArity o n => HasArity (i -> o) (Succ n)
        -- Defined at /tmp/nix-build-blog-2015-11-12-calculating_arity.html.drv-0/runghcXXXX1804289383846930886.hs:14:10
      instance HasArity t Zero
        -- Defined at /tmp/nix-build-blog-2015-11-12-calculating_arity.html.drv-0/runghcXXXX1804289383846930886.hs:17:10

Type Families

Type families are the solution we've been looking for. I originally gave up trying to understand these, after banging my head against GHC for a while. I was recently inspired to have another go, after attending a talk by Lennart Augustsson which involved some pretty hairy type-level hackery. During the course of his presentation, type families finally clicked for me, and I was able to bang out the following approach:

type family Arity t :: * where
  Arity (i -> o) = Succ (Arity o)
  Arity t        = Zero

This defines Arity as a closed type family. A type family is basically a type-level function (unlike the type-level relations encoded by multiparameter typeclasses). Type families can be open, allowing new pattern clauses to be added at any point, provided they don't overlap (just like typeclass instantiation); alternatively they can be closed, where a fixed set of, potentially overlapping, pattern clauses are used (just like function definition). We use the latter, to allow our "catch-all" pattern to overlap with the i -> o pattern.

With this type family, we can finally get the arity of each type. However, one problem still remains: the result will only be accessible at the type-level. To associate a value with each Arity type, we can use type classes; we no longer have problems with ambiguity, since we can treat all arities in the same way.

First we use the fact that our type-level numbers are singletons, i.e. they only contain one value (ignoring undefined). We use a type class to associate the name singleton :: a with the single value of type a:

class Singleton a where
  singleton :: a

instance Singleton Zero where
  singleton = Z

instance (Singleton n) => Singleton (Succ n) where
  singleton = S singleton

We can use the Singleton class to write our arity function. All of our calculation is performed by Arity at the type level, which results in either Zero or Succ n for some n; we use singleton to access the (only) value of that result type:

arity :: (Singleton (Arity a)) => a -> Arity a
arity _ = singleton

-- Handy helper functions

-- Return the arity of a value, as an Int
intArity :: (Singleton (Arity a), ToInt (Arity a)) => a -> Int
intArity = toInt . arity

-- Pretty output
format s x = concat ["Arity of '", s, "' is ", show (intArity x)]

Now, at last, we can get the arity of values:

main = mapM_ putStrLn [
    format "Bool -> Bool"           not
  , format "String"                 "hello"
  , format "Bool -> Bool -> Bool"   (&&)
  , format "(a -> b) -> [a] -> [b]" map
  ]
Arity of 'Bool -> Bool' is 1
Arity of 'String' is 0
Arity of 'Bool -> Bool -> Bool' is 2
Arity of '(a -> b) -> [a] -> [b]' is 2

It's also interesting to note the values which don't work. For example, we fail to get the arity of the identity function id :: a -> a:

main = putStrLn (format "a -> a" id)

/tmp/nix-build-blog-2015-11-12-calculating_arity.html.drv-0/runghcXXXX1804289383846930886.hs:34:18: error:
    • Ambiguous type variable ‘a0’ arising from a use of ‘format’
      prevents the constraint ‘(Singleton (Arity a0))’ from being solved.
      Probable fix: use a type annotation to specify what ‘a0’ should be.
      These potential instances exist:
        instance Singleton n => Singleton (Succ n)
          -- Defined at /tmp/nix-build-blog-2015-11-12-calculating_arity.html.drv-0/runghcXXXX1804289383846930886.hs:21:10
        instance Singleton Zero
          -- Defined at /tmp/nix-build-blog-2015-11-12-calculating_arity.html.drv-0/runghcXXXX1804289383846930886.hs:18:10
    • In the first argument of ‘putStrLn’, namely
        ‘(format "a -> a" id)’
      In the expression: putStrLn (format "a -> a" id)
      In an equation for ‘main’: main = putStrLn (format "a -> a" id)

This is because the output type of id is completely polymorphic: it could be anything, including a function. We know the arity must be at least 1, but it could be arbitrarily higher; we don't have enough information to know, and hence the compiler can't finish the calculation.

To get around this, we can restrict the output type of id. We don't have to completely monomorphise it, we just need to provide enough information to perform the type-level pattern-match for Arity:

main = mapM_ putStrLn [
    format "Bool       -> Bool      " (id :: Bool       -> Bool)
  , format "[a]        -> [a]       " (id :: [a]        -> [a])
  , format "Maybe a    -> Maybe a   " (id :: Maybe a    -> Maybe a)
  , format "(a -> [b]) -> (a -> [b])" (id :: (a -> [b]) -> (a -> [b]))
  ]
Arity of 'Bool       -> Bool      ' is 1
Arity of '[a]        -> [a]       ' is 1
Arity of 'Maybe a    -> Maybe a   ' is 1
Arity of '(a -> [b]) -> (a -> [b])' is 2