On Fri, Aug 1, 2008 at 2:55 PM, Matt Hellige <
matt@...> wrote:
> On Fri, Aug 1, 2008 at 2:40 PM, Matt Hellige <
matt@...> wrote:
>> This code compiles fine. We can even use the defined types! But if we
>> uncomment the definition of "four":
>> type four = _2 x _2
>> then we get the following:
>
> More generally, it doesn't work for squares:
> type one = _1 x _1
> type nine = _3 x _3
> These have the same problem. Does anyone see why?
>
Ok. Sorry to keep emailing myself, but I think I see what's happening.
The expansion of a type like _1 x _1 goes as follows:
_1 x _1
-> mul[_1, _1, Succ, Zero]
-> _1[apply1[_1,Succ]#It, Zero]
-> apply1[_1,Succ]#It[Zero]
-> _1[Succ,Zero]
-> Succ[Zero]
The third line seems to be the problem, as we can see by writing
type test = _1[apply1[_1,Succ]#It, Zero]
which produces the same error.
This would lead us to think maybe we can avoid the problem just by
making more aliases. Indeed we can. The following works fine:
type _1x[s[_], z] = s[z]
type _2x[s[_], z] = s[s[z]]
type _3x[s[_], z] = s[s[s[z]]]
type one = _1 x _1x
type four = _2 x _2x
type nine = _3 x _3x
But this is really ugly. So there are three questions.
1. Is this right? Can it be fixed? Can we relax the rules on illegal
cycles somehow? I have really wished for this in other cases as
well...
2. Why does this error break compilation of the other definitions in
the file? Not a big deal, maybe, but it makes it extra confusing.
3. Should I open a bug?
Thanks, and sorry for all the messages about this...
Matt
--
Matt Hellige /
matt@...
http://matt.immute.net
