Error matching types: using MultiParamTypeClasses and FunctionalDependencies to define heterogeneous-CodePudding

There is a relevant question concerning Functional Dependencies used with GADTs. It turns out that the problem is not using those two together, since similar problems arise without the use of GADTs. The question is not definitively answered, and there is a debate in the comments.

The problem

I am trying to make a heterogeneous list type which contains its length in the type (sort of like a tuple), and I am having a compiling error when I define the function "first" that returns the first element of the list (code below). I do not understand what it could be, since the tests I have done have the expected outcomes.

I am a mathematician, and a beginner to programming and Haskell.

The code

I am using the following language extensions:

{-# LANGUAGE GADTs, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances #-}

First, I defined natural numbers in the type level:

data Zero = Zero
newtype S n = S n

class TInt i
instance TInt Zero
instance (TInt i) => TInt (S i)

Then, I defined a heterogeneous list type, along with a type class that provides the type of the first element:

data HList a as where
    EmptyList :: HList a as
    HLCons :: a -> HList b bs -> HList a (HList b bs)

class First list a | list -> a
instance First (HList a as) a

And finally, I defined the Tuple type:

data Tuple list length where
    EmptyTuple :: Tuple a Zero
    TCons :: (TInt length) => a -> Tuple list length -> Tuple (HList a list) (S length)

I wanted to have the function:

first :: (First list a) => Tuple list length -> a
first EmptyTuple = error "first: empty Tuple"
first (TCons x _) = x

but it does not compile, with a long error that appears to be that it cannot match the type of x with a.

Could not deduce: a1 ~ a
      from the context: (list ~ HList a1 list1, length ~ S length1,
                         TInt length1)
        bound by a pattern with constructor:
                   TCons :: forall length a list.
                            TInt length =>
                            a -> Tuple list length -> Tuple (HList a list) (S length),
                 in an equation for ‘first’
[...]
Relevant bindings include
        x :: a1 (bound at problem.hs:26:14)
        first :: Tuple list length -> a (bound at problem.hs:25:1)

The testing

I have tested the type class First by defining:

testFirst :: (First list a) => Tuple list length -> a
testFirst = undefined

and checking the type of (testFirst x). For example:

ghci> x = TCons 'a' (TCons 5 (TCons "lalala" EmptyTuple))
ghci> :t (testFirst x)
(testFirst x) :: Char

Also this works as you would expect:

testMatching :: (Tuple (HList a as) n) -> a
testMatching (TCons x _) = x

"first" is basically these two combined.

The question

Am I attempting to do something the language does not support (maybe?), or have I stumbled on a bug (unlikely), or something else (most likely)?

CodePudding user response：

Oh dear, oh dear. You have got yourself in a tangle. I imagine you've had to battle through several perplexing error messages to get this far. For a (non-mathematician) programmer, there would have been several alarm bells hinting it shouldn't be this complicated. I'll 'patch up' what you've got now; then try to unwind some of the iffy code.

The correction is a one-line change. The signature for first s/b:

first :: Tuple (HList a as) length -> a

As you figured out in your testing. Your testFirst only appeared to make the right inference because the equation didn't try to probe inside a GADT. So no, that's not comparable.

There's a code 'smell' (as us humble coders call it): your class First has only one instance -- and I can't see any reason it would have more than one. So just throw it away. All I've done with the signature for first is put the list's type from the First instance head direct into the signature.

Explanation

Suppose you wrote the equations for first without giving a signature. That gets rejected blah rigid type variable bound by a pattern with constructor ... blah. Yes GHC's error messages are completely baffling. What it means is that the LHS of first's equations pattern match on a GADT constructor -- TCons, and any constraints/types bound into it cannot 'escape' the pattern match.

We need to expose the types inside TCons in order to let the type pattern-matched to variable x escape. So TCons isn't binding just any old list; it's specifically binding something of the form (HList a as).

Your class First and its functional dependency was attempting to drive that typing inside the pattern match. But GADTs have been maliciously designed to not co-operate with FunDeps, so that just doesn't work. (Search SO for '[haskell] functional dependency GADT' if you want to be more baffled.)

What would work is putting an Associated Type inside class First; or building a stand-alone 'type family'. But I'm going to avoid leading a novice into advanced features.

Type Tuple not needed

As @JonPurdy points out, the 'spine' of your HList type -- that is, the nesting of HLConss is doing just the same job as the 'spine' of your TInt data structure -- that is, the nesting of Ss. If you want to know the length of an HList, just count the number of HLCons.

So also throw away Tuple and TInt and all that gubbins. Write first to apply to an HList. (Then it's a useful exercise to write a length-indexed access: nth element of an HList -- not forgetting to fail gracefully if the index points beyond its end.)

I'd avoid the advanced features @Jon talks about, until you've got your arms around GADTs. (It's perfectly possible to program over heterogeneous lists without using GADTs -- as did the pioneers around 2003, but I won't take you backwards.)

CodePudding user response：

I was trying to figure out how to do "calculations" on the type level, there are more things I'd like to implement.

Ok ... My earlier answer was trying to make minimal changes to get your code going. There's quite a bit of duplication/unnecessary baggage in your O.P. In particular:

Both HList and Tuple have constructors for empty lists (also length Zero means empty list). Furthermore both those Emptys allege there's a type (variable) for the head and the tail of those empty (non-)lists.
Because you've used constructors to denote empty, you can't catch at the type level attempts to extract the first of an empty list. You've ended up with a partial function that calls error at run time. Better is to be able to trap first of an empty list at compile time, by rejecting the program.
You want to experiment with FunDeps for obtaining the type of the first (and presumably other elements). Ok then to be type-safe, prevent there being an instance of the class that alleges the non-existent head of an empty has some type.

I still want to have the length as part of the type, it is the whole point of my type.

Then let's express that more directly (I'll use fresh names here, to avoid clashes with your existing code.) (I'm going to need some further extensions, I'll explain those at the end.):

data HTuple list length  where 
    MkHTuple :: (HHList list, TInt length) => list -> length -> HTuple list length

This is a GADT with a single constructor to pair the list with its length. TInt length and types Zero, S n are as you have already. With HHList I've followed a similar structure.

data HNil       = HNil          deriving (Eq, Show) 
data HCons a as = HCons a as    deriving (Eq, Show) 
    
class HHList l
instance HHList HNil
instance HHList (HCons a as)
    
class (HHList list) =>  HFirst list a  | list -> a  where hfirst :: list -> a

-- no instance HFirst HNil      -- then attempts to call hfirst will be type error

instance                HFirst (HCons a as) a       where hfirst (HCons x xs) = x

HNil, HCons are regular datatypes, so we can derive useful classes for them. Class HHList groups the two datatypes, as you've done with TInt.

HFirst with its FunDep for the head of an HHList then works smoothly. And no instance HFirst HNil because HNil doesn't have a first. Note that HFirst has a superclass constraint (HHList list) =>, saying that HFirst applies only for HHLists.

We'd like HTuple to be Eqable and Showable. Because it's a GADT, we must go a little around the houses:

{-# LANGUAGE  StandaloneDeriving #-}
deriving instance (Eq list, Eq length)     => Eq   (HTuple list length)
deriving instance (Show list, Show length) => Show (HTuple list length)

Here's a couple of sample tuples; and a function to get the first element, going via the First class and its method:

htEmpty = MkHTuple HNil Zero
htup1   = MkHTuple (HCons (1 :: Int) HNil) (S Zero)

tfirst :: (HFirst list a) => HTuple list length -> a      -- using the FunDep
tfirst (MkHTuple list length) = hfirst list

-- > :set -XFlexibleContexts     -- need this in your session
-- > tfirst htup1        ===> 1
-- > tfirst htEmpty      ===> error: No instance for (HFirst HNil ...

But you don't want to be building tuples with all those explicit constructors. Ok, we could define a cons-like function:

thCons x (MkHTuple li le) = MkHTuple (HCons x li) (S le)

htup2   = thCons "Two" htup1

But that doesn't look like a constructor. Furthermore you really (I suspect) want something to both construct and destruct (pattern-match) a tuple into a head and a tail. Then welcome to PatternSynonyms (and I'm afraid quite a bit of ugly declaration syntax, so the rest of your code can be beautiful). I'll put the beautiful bits first: THCons looks just like a constructor; you can nest multiple calls; you can pattern match to get the first element.


htupA   = THCons 'A' THEmpty
htup3   = THCons True $ THCons "bB" $ htupA

htfirst (THCons x xs) = x

-- > htfirst htup3       ===> True

{-# LANGUAGE  PatternSynonyms, ViewPatterns, LambdaCase  #-}

pattern THEmpty = MkHTuple HNil Zero    -- simple pattern, spelled upper-case like a constructor

-- now the ugly
pattern THCons :: (HHList list, TInt length)
                  => a -> HTuple list length -> HTuple (HCons a list) (S length)
pattern THCons x tup              <- ((\case   
                                          { (MkHTuple (HCons x li) (S le) )
                                              | let tup = (MkHTuple li le)
                                                  -> (x, tup)  } )
                                                     -> (x, tup) )
    where
        THCons x (MkHTuple li le)  = MkHTuple (HCons x li) (S le)

Look first at the last line (below the where) -- it's just the same as for function thCons, but spelled upper case. The signature (two lines starting pattern THCons ::) is as inferred for thCons; but with explicit class constraints -- to make sure we can build a HTuple only from valid components; which we need to have guaranteed when deconstructing the tuple to get its head and a properly formed tuple for the rest -- which is all that ugly code in the middle.

Question to the floor: can that pattern decl be made less ugly?

I won't try to explain the ugly code; read ViewPatterns in the User Guide. That's the last -> just above the where.