[Haskell-cafe] printf using values more than once

[MigMit]

At this point I'm not sure how it is different from a simple function. The HoleyMonoid example

> holey = now "x = " . later show . now ", y = " . later show

when paired with 'argn'-style variables essentially becomes

> holey arg1 arg2 = "y = " ++ show arg2 ++ "; x = " ++ show arg1

So, what kind of syntax do you have in mind?

> On 3 Jun 2021, at 22:21, Olaf Klinke <olf at aatal-apotheke.de> wrote:
> 
> Dear Café,
> 
> since the topic recently was rendering text, I'd like to ask a related design question. I want a version of printf that
> - is more type-safe because unused or surplus arguments cause compile-time errors,
> - the formatting instructions can use arguments out of order and more than once, - is polymorphic in the text type being built: Suppose I want to build a Pandoc Block but the holes are of type Inline. The format string must therefore be able to promote the Block type's constructors to constructors with holes.
> 
> The closest match I know of is HoleyMonoid [1] but it only provides printf-like holes, whereas I need named positional arguments like arg1, arg2 etc. that can be repeated. Document templating libraries provide these, but all templating libraries I looked at are type-unsafe.
> 
> In order to fulfill the second requirement, one could use the free monad over a Reader functor, e.g.
>    Free ((->) (forall a. Show a => a)) String
> with some custom instances. Here one can use the nesting levels of the free monad to encode the argument position. But it is just as type-unsafe as printf. Funneling return type constructors through this works sort of, but it's awkward.
> 
> One can achieve type saftey with type classes like printf does:
> class Eventually r a where
>   eventually :: r -> a
> instance Eventually r r where
>   eventually = id
> instance (Eventually r a) => Eventually r (b -> a) where
>   eventually r = const (eventually r)
> 
> This class can be used to inject constant Text into any nesting of
> (Text -> ... -> Text -> Text)
> and argument position is indeed function argument position. But using this system often leads to type ambiguity errors. Also, it is so type-safe that it is impossible to write a function taking a natural number and returning the hole of the corresponding position: Such a function would be dependently-typed.
> 
> My current best implementation uses a combination of Eventually and HoleyMonoid, but I'm not entirely satisfied.
> 
> Olaf
> 
> [1] https://hackage.haskell.org/package/HoleyMonoid_______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.