relaxed instance rules spec (was: the MPTC Dilemma
claus.reinke at talk21.com
Thu Mar 2 09:53:07 EST 2006
it has been a long time since I looked into nested types so I may
well be wrong, but:
nested types allow for structures containing infinitely many types,
but you can never write down such infinity, unless by a finite
representation or an infinite process. when you want to work with
such nested types, you either use a unifiably infinity of workers
(finitely represented via polymorphic recursion) or you write a
generator for a family of workers (Blampied/Jones, Hinze).
so you have no infinite types to start with, but you may have
infinitary producers of types (and as the Mul example shows,
that may not only happen by adding stuff on the outside, but
also by refining variables in the inside). and if you connect one
of those to an otherwise terminating consumer, you might still
end up with a non-terminating inference.
my argument was -the above being the case- we should not
blame the consumers because they may be connected with
bad producers, but _only_ those bad producers themselves.
in the Mul case, Mul is fine as a consumer, but using cyclic
programming to turn it into its own producer is not.
>> - Mul recurses down a type in its second parameter
>> - types in Haskell are finite
>> - there is a non-terminating Mul inference
>> the problem is that we have somehow conjured up an infinite
>> type for Mul to recurse on without end! Normally, such infinite
>> types are ruled out by occurs-checks (unless you are working
>> with Prolog III;-), so someone forgot to do that here. why?
>> where? how?
> Polymorphic recursion allows the construction of infinite types if I
> understand what you mean. if you are clever (or unlucky) you can get
> jhcs middle end to go into an infinite loop by using them.
>> -- an infinite binary tree
>> data Bin a = Bin a (Bin (a,a))
> John Meacham - ⑆repetae.net⑆john⑈
> Haskell-prime mailing list
> Haskell-prime at haskell.org
More information about the Haskell-prime