Define lists with least fixed point, sum, and product types

Question

I want to define lists using only this type definitions:

data Unit = Unit
data Prod a b = P a b
data Sum a b = L a | R b
newtype Mu f = Mu (forall a . (f a -> a) -> a)

I succeeded defining natural numbers as follows:

zeroMu = Mu $ \f -> f $ L Unit
succMu (Mu g) = Mu $ \f -> f $ R $ g f

I know how to define lists with the help of an extra data type:

data ListF a x = NilF | ConsF a x
nilMu' = Mu $ \f -> f $ NilF
consMu' x (Mu g) = Mu $ \f -> f $ ConsF x $ g f

The 'better' I can get is this, but it does not type-checks (intended type is µL.(1+(a*L))):

nilMu = Mu $ \f -> f $ L Unit
consMu x (Mu g) = Mu $ \f -> f $ R $ P x $ g f

How can I define nilMu and consMu using only previously defined types and their constructors?

Edit

As @chi answer explains, it can be done defining a newtype as follows:

newtype F a x = F (Sum Unit (Prod a x))
nilMu = Mu $ \f -> f $ F $ L Unit
consMu x (Mu g) = Mu $ \f -> f $ F $ R $ P x $ g f

It type-checks, but requires to define a new type.

The intend of this question is to extend a simply typed combinatory logic with unit, product, sum, and recursive types. First three types are straightforward to implement introducing 7 new combinators (unit, pair, first, second, left, right, case). Recursive types seems easy to implement too, just add a type constructor combinator mu, but as this questoins shows is not flexible enough without additional language constructs.

Is there a solution to this problem? Are there combinatory logics with recursive types to consult?

Answer 1

You can not do it without an additional data or newtype, in Haskell.

To do it, one would need to write

nilMu :: Mu (\l -> S (P a l) ())
consMu :: a -> Mu (\l -> S (P a l) ()) -> Mu (\l -> S (P a l) ())

but Haskell does not allow type-level functions in this way. Mu can only be applied to a type constructor of kind * -> *, not a type-level function of the same kind.

nilMu :: Mu (F a)
consMu :: a -> Mu (F a) -> Mu (F a)

where F a is defined as an additional type

newtype F a x = F (S (P a x) ())

---

For the reason why Haskell does not allow type level functions, consider

assuming foo :: f a -> f Char
infer    foo True :: ???

One might argue that in foo True, True is a Bool, so we can infer f = \t->t and a = Bool. The result is foo True :: (\t->t) Char = Char.

One might also argue that we can infer f = \t->Bool and a = String, and that the result is foo True :: (\t->Bool) Char = Bool

In general, we do not like that. We want type inference to proceed by pattern matching f and a against the actual type. For that, we want both f and a to have a correspondent "obvious" name in the actual type.

For what it is worth, you can do this in dependently type languages, such as Coq, Agda, Idris, etc. There, type inference will not work on code like foo True above, since f can not be inferred. Worse, in these languages, if bar :: f a -> ... and we call bar [True], then f could fail to be inferred to [] because this is not the only solution (they do have good heuristics, though, which often work anyway, even if the general problem is undecidable).