undefined | Better HN

0 pointsmoomin11y ago0 comments

I think what the author ultimately means is "well behaved transducers are equivalent to functions of the form a->[b] (modulo state) and therefore form a category".

True story: the transducer announcement has mostly made me read up on the Haskell fold and lens libraries...

0 comments

tel11y ago

If you think of Transducers as

    type Transducer a b = 
      forall r . (b -> r -> r) -> (a -> r -> r)

(And I'm not claiming this is correct) then you can reasonably easily show that this is isomorphic to (a -> [b])

    forall r . (b -> r -> r) -> (a -> r -> r)
    forall r . (r -> b -> r) -> (r -> a -> r)
    a -> (forall r . (r -> b -> r) -> r -> r)  [non-obvious, but true]
    a -> [b]

This is "obviously" the Kleisli category for [] so you get rich, rich structure here. If you want to include local state such as what's needed to implement `take` then you can do something like

    data Fold i o where
      Fold :: (i -> x -> x) -> x -> (x -> o) -> Fold i o

    type Transducer a b = forall r . Fold b r -> Fold a r

If you're familiar with pure profunctor lenses then I can tell you that Fold is a Profunctor and thus these can be acted on by a lot of generalized lens combinators. This explains a lot of the richness.

DanWaterworth11y ago

Here's proof that the last two parts are isomorphic:

    to :: (a -> [b]) -> (a -> (forall r . (b -> r -> r) -> r -> r))
    to f a =
      h (f a)
     where
      h :: [b] -> (forall r . (b -> r -> r) -> r -> r)
      h b cons nil =
        case b of
          (x:xs) -> cons x (h xs cons nil)
          [] -> nil

    from :: (a -> (forall r . (b -> r -> r) -> r -> r)) -> (a -> [b])
    from f a = f a (:) []

moominOP11y ago

Is this quite right? Sorry this is a bit vague/unclear, but what happens if you, say, call the reduction function, throw the result away and then call it again?

I ran this example through Clojure in let's write a transducer, and it plain doesn't work; I think the mapping given above works for all transducers that are actually valid, but I think the type definition allows for broken ones.

Again, I'm not sure & still learning, so please explain if I've gone wrong here.

1 more reply

tel11y ago

The fast way is to say that [b] is the initial algebra of the functor (Maybe . (b,)) and then note that initial algebras are representable as

    newtype Mu f = Mu (forall r . (f r -> r) -> r)

1 more reply

NotAtWork11y ago

Thank you.

That step had me really confused.

j / k navigate · click thread line to collapse

0 comments

tel11y ago

If you think of Transducers as

    type Transducer a b = 
      forall r . (b -> r -> r) -> (a -> r -> r)

(And I'm not claiming this is correct) then you can reasonably easily show that this is isomorphic to (a -> [b])

    forall r . (b -> r -> r) -> (a -> r -> r)
    forall r . (r -> b -> r) -> (r -> a -> r)
    a -> (forall r . (r -> b -> r) -> r -> r)  [non-obvious, but true]
    a -> [b]

This is "obviously" the Kleisli category for [] so you get rich, rich structure here. If you want to include local state such as what's needed to implement `take` then you can do something like

    data Fold i o where
      Fold :: (i -> x -> x) -> x -> (x -> o) -> Fold i o

    type Transducer a b = forall r . Fold b r -> Fold a r

DanWaterworth11y ago

Here's proof that the last two parts are isomorphic:

    to :: (a -> [b]) -> (a -> (forall r . (b -> r -> r) -> r -> r))
    to f a =
      h (f a)
     where
      h :: [b] -> (forall r . (b -> r -> r) -> r -> r)
      h b cons nil =
        case b of
          (x:xs) -> cons x (h xs cons nil)
          [] -> nil

    from :: (a -> (forall r . (b -> r -> r) -> r -> r)) -> (a -> [b])
    from f a = f a (:) []

moominOP11y ago

Is this quite right? Sorry this is a bit vague/unclear, but what happens if you, say, call the reduction function, throw the result away and then call it again?

Again, I'm not sure & still learning, so please explain if I've gone wrong here.

1 more reply

tel11y ago

The fast way is to say that [b] is the initial algebra of the functor (Maybe . (b,)) and then note that initial algebras are representable as

    newtype Mu f = Mu (forall r . (f r -> r) -> r)

1 more reply

NotAtWork11y ago

Thank you.

That step had me really confused.

j / k navigate · click thread line to collapse