26 Feb
2007
26 Feb
'07
11:35 a.m.
On Mon, Feb 26, 2007 at 04:35:06PM +0100, Pepe Iborra wrote:
First, via existentials:
appendL1 :: List a t1 -> List a t2 -> exists t3. List a t3
It seems like this problem is begging for the new indexed types (for which I never remember the right syntax). type AddListTs :: * -> * -> * AddListTs NilT NilT = NilT AddListTs NilT t = t AddListTs (ConsT t) t' = AddListTs t (ConsT t') then appendLi :: List a t1 -> List a t2 -> List a (AddListTs t1 t2) I'd be interested if Manuel had an idea whether this would work right. I think it can be made equivalent to the FD approach, but doesn't require that you define a "stupid" class, and is far, far prettier. -- David Roundy Department of Physics Oregon State University