2
$\begingroup$

In the paper Total Functional Programming by D.A. Turner three rules are given for a programming language to remain total:

  1. complete case analysis
  2. covariant type recursion (type constructor should not appear in negative position in a constructor argument)
  3. structural recursion

But with these rules I can still have an infinite loop:

data Fix f = Fix (f (Fix f))
data Bad r = Bad (r -> r)

bad :: Fix Bad -> Fix Bad
bad b =
  case b of
    Fix t ->
      case t of
        Bad f -> f b

nonTotal = bad (Fix (Bad bad))

Where is my mistake? Should all type variables also only appear covariantly? Or is the "covariant type recursion" condition more strict?

$\endgroup$
2
$\begingroup$

The constraint

  1. covariant type recursion (type constructor should not appear in negative position in a constructor argument)

excludes this

data Bad r = Bad (r -> r)
                  ^    ^--- positive position
                  ^-------- negative position

Indeed, all the occurrences of r must appear in positive position.

Should all type variables also only appear covariantly?

Yes, precisely.

Essentially, your Fix Bad tries to generate a type $T$ isomorphic to $T \to T$. If we had that, we would have a model of the untyped $\lambda$ calculus, where terms are not normalizing ("terminating") in general.

Indeed, to apply any two terms $x, y : T$ we can exploit the isomorphism to treat $x$ as if $x : T\to T$, at which point the application $x y$ becomes feasible. As a special case, we also obtain $xx$, hence $\Omega = (\lambda x.xx)(\lambda x.xx)$ which is the archetypal non normalizing term.

To conclude let me point out that, in some advanced calculi with dependent types, covariant recursion is not enough, and you need an even stricter constraint called "strict positivity". Without that, contradictions arise. In Haskell-like languages, covariance (and the other constraints you mention) should suffice.

$\endgroup$
  • $\begingroup$ Thanks! So that means Fix is still valid? And the type "data Mu f = Mu (forall t. (f t -> t) -> t) is also valid (f only occurs positively). Correct? $\endgroup$ – Labbekak Jun 21 '18 at 19:14
  • $\begingroup$ @Labbekak No, Fix is not valid, either. Fix f is defined as f (Fix f) which is not a positive occurrence of Fix f (nor a negative one). Coq would reject that. After all it could be negative or positive or neither depending on what f is, and we do not know that at this point. Mu f is not explicitly recursive, so that would be valid, and you can use that in, say, Coq. (However, I think that Mu f might not be isomorphic to f (Mu f)when f is not covariant). $\endgroup$ – chi Jun 21 '18 at 19:45
  • $\begingroup$ @Labbekak Note that negative/non positive uses of a type variable are allowed, as long as you do not take the fixed point on that. So, in these cases you should not consider whether f occurs positively or not. Further, for writing these types, you need higher kinds, and the paper you mention does not consider that (I think). $\endgroup$ – chi Jun 21 '18 at 19:51
  • $\begingroup$ Is there an algorithm that I can use to check for (non-strict) positivity of an ADT? I am honestly pretty confused at the moment how to check if an ADT is valid or not. Can I check an ADT or should I check for the specific uses of a type? $\endgroup$ – Labbekak Jun 21 '18 at 20:27
  • $\begingroup$ @Labbekak I'm not following you completely. Usually, you take a recursive type definition like data T x y = K (... (T x' y') ...(T x'' y'')...) | ... and check whether those occurrences are in positive position. That's it. Fix can not be defined according to these rules, even if it could be used on covariant functors, which would cause no harm. Fix is disallowed because if we had it we could also use it badly, on noncovariant fs. $\endgroup$ – chi Jun 21 '18 at 20:38

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.