Hello,
I am trying to understand the definition of (co)inductive types in
Haskell. After reading the beginning of Vene's thesis [1] I was happy,
because I understood the definition of the least fixpoint:
newtype Mu f = In (f (Mu f)).
But this definition coincides with his definition of the great
On Tuesday 17 March 2009 7:36:21 pm ben wrote:
> I am trying to understand the definition of (co)inductive types in
> Haskell. After reading the beginning of Vene's thesis [1] I was happy,
> because I understood the definition of the least fixpoint:
>
> newtype Mu f = In (f (Mu f)).
>
> But this de
On Tue, Mar 17, 2009 at 4:36 PM, ben wrote:
> Then I stumbled over a blog entry of Shin-Cheng Mu [2] and from there
> over an article of Wadler [3], where the least fixpoint is encoded as
>
> Lfix X. F X = All X. (F X -> X) -> X.
>
> and the greatest fixpoint as
>
> Gfix X. F X = Exists X. (X
On Wed, 2009-03-18 at 03:22 -0400, Dan Doel wrote:
> On Tuesday 17 March 2009 7:36:21 pm ben wrote:
> > I am trying to understand the definition of (co)inductive types in
> > Haskell. After reading the beginning of Vene's thesis [1] I was happy,
> > because I understood the definition of the least
One typo correction:
On Wed, Mar 18, 2009 at 2:15 AM, Ryan Ingram wrote:
> Let "Pair a b" be an abbreviation for "forall c. (a -> b -> c)",
This should say that Pair a b is an abbreviation for
forall c. (a -> b -> c) -> c
-- ryan
___
Haskell-Cafe
Hi Ben,
But this definition coincides with his definition of the greatest
fixpoint
In Haskell the least and greatest fixed points coincide.
(Categorically, this is called "algebraically compact" I think). You
can still "fake" coinductive types to some degree by consistently
using unfold
On Wed, Mar 18, 2009 at 5:15 AM, Ryan Ingram wrote:
> newtype Lfix f = Lfix (forall x. (f x -> x) -> x)
>
> l_in :: Functor f => f (Lfix f) -> Lfix f
> l_in fl = Lfix (\k -> k (fmap (\(Lfix j) -> j k) fl))
> -- derivation of l_in was complicated!
I found l_in easiest to write in terms of cata and
On Wed, Mar 18, 2009 at 8:10 AM, David Menendez wrote:
> l_out :: Functor f => Lfix f -> f (Lfix f)
> l_out = cata (fmap l_in)
>
> g_in :: Functor f => f (Gfix f) -> Gfix f
> g_in = ana (fmap g_out)
Well, you just blew my mind. I had an informal proof in my head of
why g_in shouldn't be possible
Thanks a lot to all of you for your help.
It took some time for me to realize that the only difference between
Vene and Wadler is in fact, that Wadler has an explicit representation
for the fixpoints - which answers the question of existence.
I will spend some more time on digesting all the infor
On Wednesday 18 March 2009 5:28:35 am Duncan Coutts wrote:
> You can explain it to yourself (not a proof) by writing out the example
> for lists and co-lists along with fold for the list and unfold function
> for the co-list. Then write conversion functions between them. You can
> go from lists to
On Wednesday 18 March 2009 5:15:32 am Ryan Ingram wrote:
> There's something from Wadler's draft that doesn't make sense to me. He
> says:
>
> > This introduces a new type, T = Lfix X. F X, satisfying the isomorphism
> > T ~ F T. Note that it is an isomorphism, not an equality: the type
> > come
On Wed, Mar 18, 2009 at 8:10 AM, David Menendez wrote:
> l_out :: Functor f => Lfix f -> f (Lfix f)
> l_out = cata (fmap l_in)
>
> g_in :: Functor f => f (Gfix f) -> Gfix f
> g_in = ana (fmap g_out)
OK, I understand these now.
But they both seem to have significant performance implications, whic
12 matches
Mail list logo
