Termination

[thumphries]

Ideally it would be provably impossible to construct a template that diverges.

However, recursive datatypes and named recursion / corecursion will make this hard to achieve. Notes on related tricks and compromises will go here.

[thumphries]

I'm pretty sure we will need a totality checker if we want to keep those features (and we do).

sdbo says:

Totality checking is necessary when you have recursive
binding but want to act as though those bindings can only do folds on
data and unfolds on codata.

http://stackoverflow.com/questions/25255413/how-did-haskell-add-turing-completeness-to-system-f

Which is exactly what we want to do. Will investigate if this will be difficult. Can be retrofit after the rest is loosely in place.

[thumphries]

data Bad a = Bad (Bad a -> a)

apply :: Bad a -> a
apply x = case x of Bad f -> f x

fix :: (a -> a) -> a
fix f = apply (Bad (\ x -> f (apply x)))

No sensible recursion principle can be derived for Bad, so it should be rejected.

If we reject any datatype that is recursive in a negative position, only well-founded recursion is admitted.

Good description of positive v negative polarity here http://cs.stackexchange.com/questions/42150/meaning-of-positive-position-and-negative-position-in-type-theory

Note that this doesn't mean anything particularly sinister for our usual collection of recursive datatypes. This check can probably even be omitted.

---

Neater explanation from Wadler, Recursive Types for Free!:

Adding recursive types can alter the nature of a type system. The polymorphic lambda calculus has the pleasant propery of being strongly normalising: all reduction sequences terminate in a normal form. But augmenting this calculus with the type

Lfix X. 1 + (X -> X)

has the unpleasant consequence of introducing terms with no normal form. Fortunately, strong normalisation can be preserved by a mild restriction: don't allow the recursive type variable to appear in a negative position. The example violates this constraint, because the recursive type variable X appears to the left of the function arrow.

Thus, it is safe to extend the polymorphic lambda calculus by adding least fixpoint types with type variables in positive position.

[thumphries]

Named recursion: might be able to just compute the call graph and check it's a DAG.

[tranma]

This makes sense. We only need data definitions to be checked for strict positivity like you said, and a totality checker that allows only primitive recursion (and structural recursion, probably).

I find the Agda wiki very helpful here, esp. with the implementation details. You've probably already seen those, just linking them here for reference:

http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Totality
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.SimpleInductiveTypes

[thumphries]

Design status

Will need to write a positivity check as part of data declarations. This seems pretty straightforward, structural check.

Will need letrec for various reasons. To retain totality I'm planning the following restrictions:

• Call graph must form a DAG (just build the graph and try to sort it topologically, excluding reflexive loops)
• Self-calls must take place on at least one component of the arguments, i.e. something bound with a Con pattern in a case statement.
  • this will be pretty coarse and syntactic at first. I will probably just ban self-calls until someone needs them.

eventually it would be nice to remove the DAG restriction in favour of some type cardinality system, pretty low on the priorities though

[thumphries]

Without HKT we only have to worry about this kind of _|_

data Bad = Bad (Bad -> Bool)

bot :: Bad -> Bool
bot b =
  case b of Bad f -> f b

positivity check is done, just needs to be sped up a little bit, the naive implementation runs in exponential time

[thumphries]

This has been neglected as it's essentially my hobby component of the project, not important for prod. Will revisit in spare cycles. All that's needed is a (fast) positivity check and a test for structural recursion, I think?

In practice we have syntactic restrictions and the DAG requirement, which make it very difficult to construct a fixpoint from a template.