CODEWITHSUNDEEP
haskell
Lemming
Lemming

Reputation: 4205

Ambiguous type variable in length of heterogeneous list

I have an issue with ambiguous type variables when computing the length of a heterogeneous list. The problem seems to be that the length-function is not polymorphic in the HList's elements.

My Code

First, all the language extensions I'm using:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE NoMonomorphismRestriction #-}

Natural numbers are defined like so:

data Nat = Zero | Succ Nat

data HNat n where
    HZero :: HNat Zero
    HSucc :: HNat n -> HNat (Succ n)

The heterogeneous list is defined as a GADT

data HList (ts :: [*]) where
    HNil  :: HList '[]
    (:::) :: t -> HList ts -> HList (t ': ts)
infixr 5 :::

We can query the length of an HList:

class HLength xs n | xs -> n where
    hLength :: HList xs -> HNat n

instance HLength '[] Zero where
    hLength HNil = HZero

instance HLength xs n => HLength (x ': xs) (Succ n) where
    hLength (_ ::: xs) = HSucc (hLength xs)

We can index into an HList and retrieve the i-th element:

class HIndex xs i y | xs i -> y where
    hIndex :: HList xs -> HNat i -> y

instance HIndex (x ': xs) Zero x where
    hIndex (x ::: xs) HZero = x

instance HIndex xs i y => HIndex (x ': xs) (Succ i) y where
    hIndex (x ::: xs) (HSucc i) = hIndex xs i

The Issue

With that established I'll demonstrate the issue.

Suppose I construct an HList containing a function that itself takes an HList and does something with its first element.

test1 = ((\l n -> l `hIndex` HZero || n == 0) ::: HNil)

In this case the first element has to be a Bool. The derived type-signature confirms that constraint:

:: (Eq a, Num a, HIndex xs 'Zero Bool) =>
    HList '[HList xs -> a -> Bool]

Now I would like to calculate the length of the list test:

test2 = hLength test1

Unfortunately, this fails to compile with the following error message:

HListConstraints.hs:55:17:
    No instance for (HIndex xs0 'Zero Bool)
      arising from a use of ‘test1’
    The type variable ‘xs0’ is ambiguous
    Note: there is a potential instance available:
      instance HIndex (x : xs) 'Zero x
        -- Defined at HListConstraints.hs:42:10
    In the first argument of ‘hLength’, namely ‘test1’
    In the expression: hLength test1
    In an equation for ‘test2’: test2 = hLength test1
Failed, modules loaded: none.

The constraint on the list elements causes ambiguous type variables.

My understanding is that I need to make hLength polymorphic in the elements of the list that is passed to it. How can I do that?

Upvotes: 4

Views: 178

Answers (2)

justinpc
justinpc

Reputation: 825

Alternatively, we could explicitly define the type of test1 to be test1 :: HList ((HList (Bool ': xs) -> Int -> Bool) ': '[]) alone.

This allows us to leave the instance definitions as they were, and do away with the type equality constraints of form xs ~ (x ': xs') which András proposes.

The choice is then whether you want to have to explicitly define the type of test1. The type equality constraints make it possible to define test1 without also providing a type annotation.

Upvotes: 0

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

Reputation: 30103

The problem isn't with HLength, and it's already as polymorphic as it can be. The issue is with HIndex, which is unnecessarily specific in the xs parameter.

From HIndex xs 'Zero Bool we should be able to infer that xs has Bool ': xs' shape for some xs'. Since the HIndex implementation is driven by the Nat class parameter, we can leave the other parameters unspecified in the instance heads, and instead refine them in the instance constraints, enabling GHC to do the mentioned inference:

class HIndex xs i y | xs i -> y where
    hIndex :: HList xs -> HNat i -> y

instance (xs ~ (x ': xs')) => HIndex xs Zero x where
    hIndex (x ::: xs) HZero = x

instance (xs ~ (y ': xs'), HIndex xs' i x) => HIndex xs (Succ i) x where
    hIndex (x ::: xs) (HSucc i) = hIndex xs i

After this:

test1 :: (Eq a, Num a) => HList '[HList (Bool : xs') -> a -> Bool]

The HIndex constraint disappears, and the remaining constraints are resolved when Num a makes a default to Integer:

> :t hLength test1
hLength test1 :: HNat ('Succ 'Zero)

The general rule when computing with type classes is to move type dependencies into instance constraints, and only do those pattern matches in instance heads which are essential to instance definitions. This turns instance head matching problems (which immediately fail when parameters aren't of the right form) into constraint solving problems (which can be lazily solved based on information from other parts of the program).

Upvotes: 4

Related Questions