Unfoldr, Replicate (and possibly something more)

[gspia]

Hi

Would Unfoldr possibly fit in into this lib?

It could be defined like

data Unfoldr :: (b -> Exp (Maybe (a,b))) -> b -> Exp [a]

data UnfoldrStop :: Maybe (a,b) -> Exp [a]
type instance Eval (UnfoldrStop ('Just '(a,b))) = '[a]
type instance Eval (UnfoldrStop 'Nothing) = '[]

data StepRec :: (b -> Exp (Maybe (a,b))) -> Maybe (a,b) -> Exp [a]
type instance Eval (StepRec  f ('Just '(a,b))) = Eval (Unfoldr f b)
type instance Eval (StepRec  _ 'Nothing) = '[]

data UnfoldrCase :: (b -> Exp (Maybe (a,b))) -> Maybe (a,b) -> Exp [a]
type instance Eval (UnfoldrCase f ('Just '(a,b))) =
    Eval (Eval (UnfoldrStop ('Just '(a,b))) Fcf.++ Eval (StepRec f ('Just '(a,b))))
type instance Eval (UnfoldrCase _ 'Nothing) = '[]

-- type instance Eval (Unfoldr (f :: b -> Exp (Maybe (a, b))) c ) =
-- Note, if we wrote the above type instance, then the last parameter cannot
-- have 'b' as a name. Why?
type instance Eval (Unfoldr f c) =
    Eval (If (Eval (IsJust (f @@ c)))
         ( Pure (Eval (UnfoldrCase f Fcf.=<< Pure (f @@ c) ) ) )
         ( Pure '[] )
         )

-- to make an example
data ToThree :: Nat -> Exp (Maybe (Nat,Nat))
type instance Eval (ToThree b) = Eval
    (If ( Eval ( b Fcf.>= 4) )
        (Pure Nothing)
        (Pure (Just '(b, b TL.+ 1 )))
    )
-- :kind! Eval (Unfoldr ToThree 0)

After that, it is possible to define hylomorphism for type level lists:

-- Hylomorphism is anamorphism (psi) followed by catamorphism (phi).
-- Close but not quite:
data HyloList :: (a -> b -> Exp b) -> (b -> Exp (Maybe (a,b))) -> b -> Exp b
-- b and [a] to give b in phi    and  b to give [a] in psi
type instance Eval (HyloList phi psi b) = Eval (Foldr phi b Fcf.=<< Unfoldr psi b)

and Iterate and Factorial etc.

data NumIter :: a -> Nat -> Nat -> Exp (Maybe (a,Nat))
type instance Eval (NumIter a s b) = Eval
    (If ( Eval ( b Fcf.>= s) )
        (Pure Nothing)
        (Pure (Just '( a, b TL.+ 1 )))
    )

data TTimes1 :: Nat -> Nat -> Exp (Maybe (a,Nat))
type instance Eval (TTimes1 t s) = Eval (NumIter s t s)

type Fact2 t = HyloList NatProd (TTimes1 t) 1 

-- :kind! Eval (Fact2 10)

type Replicate n a = Unfoldr (NumIter a n) 0
-- :kind! Eval (Iterate 6 "hmm")
-- :kind! Eval (Iterate 6 2)
-- :kind! Eval (Iterate 6 '("hmm",2))

The following gist contains headers and the above definitions in one place:

unfoldr gist

[Lysxia]

Great idea! I would be happy to add Unfoldr and Iterate. Would you like to make a PR?

The definition of Unfoldr could be simplified a little, with only two families, one to apply the coalgebra, and one to pattern-match on it.

---

> -- type instance Eval (Unfoldr (f :: b -> Exp (Maybe (a, b))) c ) =
> -- Note, if we wrote the above type instance, then the last parameter cannot
> -- have 'b' as a name. Why?
> type instance Eval (Unfoldr f c) =

The name b is already taken for the kind of the argument of f, which is also the kind of c.

[gspia]

Thanks for the suggestion & ok, I can try to prepare a PR.

About the names: I just realized that it wasn't Iterate but rather Replicate.

I'll try to simplify the Unfoldr and it leaves less badly named helper families then in there. In my first trial I tried to write directly a recursive version but then the evaluation of Unfoldr just diverged to somewhere... Still don't exactly, why it didn't work and why there is this need of "indirection" (=use of helper families). I think it is conceptually something that could be elaborated more for people to be aware of that kind of "corner" cases. But how?

Anyhow, how about the examples? Maybe just put them into the haddocks so that people can quickly start playing with them? (I'll prepare the PR this way and of course I'm ready to modify or remove them if not ok.)

For lists, it is easy to also define Concat and ConcatMap. Those actually proved already to be quite useful. I'll add them at the same time.

[gspia]

Ok, the PR is now merged so it is probably ok to close this one.

[Lysxia]

Thanks! (Closed by #16)

In a PR you can use keywords to link it to an issue so it gets closed automatically. So for example you make a PR and in the message on github you can write "Closes #15" in plain text.

https://github.blog/2013-05-14-closing-issues-via-pull-requests/