[Haskell-cafe] Re: Mux, was Re: Clearly, Haskell is ill-founded
apfelmus at quantentunnel.de
Thu Jul 19 06:51:14 EDT 2007
Conor McBride wrote:
> Derek Elkins wrote:
>> As an inductive data type, isn't this empty?
> Not in the manner which I intended. But it's a good question whether what I
> wrote unambiguously represented what I intended. In full-on nuspeak, I
> Mux = Nu mux. Mu muy. /\x y. Either (y, muy x y) (x, mux y x)
> with the inductive definition nested inside the coinductive one, so that
> we always eventually twist. Just once a summer, perhaps. I've basically
> written Stefan's version, exploiting fixpoints at kind * -> * -> * to
> deliver the symmetry by the twisted :~ constructor.
I too thought that the Mu fixed point should be empty since it's missing
a base case. But that's not correct:
Mu muy . /\ x y. Either (y, muy x y) (x, mux y x)
~ Mu muy . /\ y . Either (y, muy y) (Constant1, Constant2 y)
~ Mu muy . Either (Constant3 , muy) Constant4
The result is just a list of Constant3s that ends with a Constant4
instead of . In other words, Constant4 = (x, mux y x) is the base
case for the induction. Very cunning!
> Nesting the other way around, we get this rather odd beast
> Xum = Mu muy. Nu mux. /\x y. Either (y, muy x y) (x, mux y x)
> which isn't empty either. Rather, it only allows finitely many uses of :-
> before it settles down to use :~ forever. That is, we eventually always
> twist. So this way round allows the fair multiplexer, but not the slightly
> biased one which produces two xs for every y.
> All of which goes to show that mixed co/programming is quite a sensitive
> business, and it's easy to be too casual with notation.
Can the order of quantifiers be deduced from the declarations?
codata Mux x y = Mux (Muy x y)
data Muy x y = y :- Muy x y | x :~ Mux y x
Probably, since Xum would be declared as
data Yum x y = Yum (Xum x y)
codata Xum x y = y :- Yum x y | x :~ Xum y x
More information about the Haskell-Cafe