Search code examples
haskelltypesalgebraic-data-types

Why does a sum-type of `a` containing a list constructor not match a list of `a`?


I am trying to implement primitive recursive functions. As apparently it is not common to use variadic functions in Haskell I use a type

data PrimT a = Sgl a | Sqc [a]

so I can pass atomic values and lists of values to functions. This works alright for the zero function, projection, and the successor function:

zero k (Sqc args) = if length args == k then Right 0 else Left "invalid number of arguments"
zero 1 (Sgl arg)  = Right 0

pi i k (Sqc args) = if length args == k then Right $ args!!i else Left "invalid number of arguments"
pi 1 1 (Sgl arg) = Right arg

nu (Sgl i) = Sgl $ i + 1

But I am getting problems with composition (here o). The idea behind this definition is that composition can happen with a function f and: 1) a list of functions and a list of arguments, 2) a list of functions and one argument, 3) one function and a list of arguments and finally 4) one function and one argument. Therefore I put the functions and in a PrimT so I can have cases for Sqc gs for a list of functions and Sgl g for a single function. Same for the arguments: Sqc args and Sgl arg.

o :: PrimT (PrimT b -> PrimT c) -> PrimT (PrimT a -> PrimT b) -> PrimT a -> PrimT c
o (Sgl f) (Sqc gs) (Sqc args) = f [g args | g <- gs]
-- o (Sgl f) (Sqc gs) (Sgl arg) = f [g arg | g <- gs]
-- o (Sgl f) (Sgl g) (Sqc args) = f [g args]
-- o (Sgl f) (Sgl g) (Sgl arg) = f [g arg]

However the compiler is not happy with the part f [g args | g <- gs]. It says:

primrec.hs:69:35: error:
    • Couldn't match expected type ‘PrimT b’
                  with actual type ‘[PrimT b]’
    • In the first argument of ‘f’, namely ‘[g args | g <- gs]’
      In the expression: f [g args | g <- gs]
      In an equation for ‘o’:
          o (Sgl f) (Sqc gs) (Sqc args) = f [g args | g <- gs]
    • Relevant bindings include
        gs :: [PrimT a -> PrimT b] (bound at primrec.hs:69:16)
        f :: PrimT b -> PrimT c (bound at primrec.hs:69:8)
        o :: PrimT (PrimT b -> PrimT c)
             -> PrimT (PrimT a -> PrimT b) -> PrimT a -> PrimT c
          (bound at primrec.hs:69:1)
   |
69 | o (Sgl f) (Sqc gs) (Sqc args) = f [g args | g <- gs]
   |                                   ^^^^^^^^^^^^^^^^^^

primrec.hs:69:38: error:
    • Couldn't match expected type ‘PrimT a’ with actual type ‘[a]’
    • In the first argument of ‘g’, namely ‘args’
      In the expression: g args
      In the first argument of ‘f’, namely ‘[g args | g <- gs]’
    • Relevant bindings include
        g :: PrimT a -> PrimT b (bound at primrec.hs:69:45)
        args :: [a] (bound at primrec.hs:69:25)
        gs :: [PrimT a -> PrimT b] (bound at primrec.hs:69:16)
        o :: PrimT (PrimT b -> PrimT c)
             -> PrimT (PrimT a -> PrimT b) -> PrimT a -> PrimT c
          (bound at primrec.hs:69:1)
   |
69 | o (Sgl f) (Sqc gs) (Sqc args) = f [g args | g <- gs]
   |

But I don't understand why. PrimT a can be a list of a ([a]) according to its definition. So where is the problem?


Solution

  • PrimT a can be a list of a ([a]) according to its definition

    No, PrimT a can either be an Sgl or an Sqc. So given a list xs of type [a], Sqc xs would be a PrimT a, but xs would not. xs is already a list - it can't also be something else.

    By that same logic Sqc args is a PrimT a and Sqc [g (Sqc args) | g <- gs] is a PrimT (PrimT b), but without the Sqc they're just lists.

    I should also point out that PrimT (PrimT b) isn't the type that you want (you want PrimT b), so you'll still need to flatten the result to get what you want.