17 Jul
2007
17 Jul
'07
12:42 p.m.
On Tue, 2007-07-17 at 13:23 +0100, Conor McBride wrote:
On 16 Jul 2007, at 19:53, Stefan Holdermans wrote:
I wrote:
I came up with [...]
apfelmus' solution is of course more elegant, but I guess it boils down to the same basic idea.
Yep, you need inductive data to guarantee that you eventually stop spitting out one sort of thing and flip over to the other. Here's my version.
Mux...
data{-codata-} Mux x y = Mux (Muy x y)
...is defined by mutual induction with...
data Muy x y = y :- Muy x y | x :~ Mux y x
As an inductive data type, isn't this empty?