| > Is there any way to define type-level multiplication without requiring | > undecidable instances? | | No, not at the moment. The reasons are explained in the paper "Type | Checking with Open Type Functions" (ICFP'08): | | http://www.cse.unsw.edu.au/~chak/papers/tc-tfs.pdf | | We want to eventually add closed *type families* to the system (ie, | families where you can't add new instances in other modules). For | such closed families, we should be able to admit more complex | instances without requiring undecidable instances. It's also worth noting that while "undecidable" instances sound scary, but all it means is that the type checker can't prove that type inference will terminate. We accept this lack-of-guarantee for the programs we *run*, and type inference can (worst case) take exponential time which is not so different from failing to terminate; so risking non-termination in type inference is arguably not so bad. Simon

On Tue, Oct 13, 2009 at 9:37 AM, Simon Peyton-Jones wrote:

| > Is there any way to define type-level multiplication without requiring | > undecidable instances? | | No, not at the moment. The reasons are explained in the paper "Type | Checking with Open Type Functions" (ICFP'08): | | http://www.cse.unsw.edu.au/~chak/papers/tc-tfs.pdfhttp://www.cse.unsw.edu.au/%7Echak/papers/tc-tfs.pdf | | We want to eventually add closed *type families* to the system (ie, | families where you can't add new instances in other modules). For | such closed families, we should be able to admit more complex | instances without requiring undecidable instances.

It's also worth noting that while "undecidable" instances sound scary, but all it means is that the type checker can't prove that type inference will terminate. We accept this lack-of-guarantee for the programs we *run*, and type inference can (worst case) take exponential time which is not so different from failing to terminate; so risking non-termination in type inference is arguably not so bad.

Some further details to shed some light on this topic. "Undecidable" instances means that there exists a program for which there's an infinite reduction sequence. By "undecidable" I refer to instances violating the conditions in the icfp'08 and in the earlier jfp paper "Understanding Functional Dependencies via Constraint Handling Rules". Consider the classic example Add (Succ x) x ~ x --> Succ (Add x x) ~ x substitute for x and you'll get another redex of the form Add (Succ ..) ... and therefore the reduction won't terminate To fix this problem, i.e. preventing the type checker to non-terminate, we could either (a) spot the "loop" in Add (Succ x) x ~ x and reject this unsatisfiable constraint and thus the program (b) simply stop after n steps The ad-hoc approach (b) restores termination but risks incompleteness. Approach (a) is non-trivial to get right, there are more complicated loopy programs where spotting the loops gets really tricky. The bottom line is this: Running the type checker on "undecidable" instances means that there are programs for which - the type checker won't terminate, or - wrongly rejects the program (incompleteness) So, the situation is slightly more scary, BUT programs exhibiting the above behavior are (in my experience) rare/contrived. -Martin

Reid Barton:

On Sat, Oct 10, 2009 at 02:59:37PM -0400, Brad Larsen wrote:

...

Suppose we implement type-level naturals as so:

data Zero data Succ a

Then, we can reflect the type-level naturals into a GADT as so (not sure if ``reflect'' is the right terminology here):

data Nat :: * -> * where Zero :: Nat Zero Succ :: Nat a -> Nat (Succ a)

Using type families, we can then proceed to define type-level addition:

type family Add a b :: * type instance Add Zero b = b type instance Add (Succ a) b = Succ (Add a b)

Is there any way to define type-level multiplication without requiring undecidable instances?

I hesitate to contradict Manuel Chakravarty on this subject... but I posted a type-level multiplication program without undecidable instances on this list in June:

http://www.haskell.org/pipermail/haskell-cafe/2009-June/062452.html

If you prefer to use EmptyDataDecls, you can replace the first four lines by

data Z data S n

data Id :: * -> * data (:.) :: (* -> *) -> (* -> *) -> (* -> *)

And I still don't understand why that definition works while the obvious one doesn't :)

Ok, I should have been more precise. It's not that anything about multiplication as such is a problem. However, when you look at the standard definitions for addition

type family Add a b :: * type instance Add Zero b = b type instance Add (Succ a) b = Succ (Add a b)

and multiplication

type family Mul a b :: * type instance Mul Zero b = Zero type instance Mul (Succ a) b = Add (Mul a b) b

then the difference is that multiplication uses nested applications of type families (namely, Add (Mul a b) b). It is this nested application of type families that can be abused to construct programs that lead to non-termination of type checking (by exploiting the openness of type families in combination with local equalities introduced either by equality constraints in type signatures or GADT pattern matches). Unfortunately, there doesn't seem to be a simple syntactic criterion that would let GHC decide between harmless and problematic uses of nested *open* family applications in family instances. Hence, we need to rule them all out. You circumvent that problem cleverly by the use of higher-kinded types. Manuel