printf using values more than once

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

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
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.

On Thu, 3 Jun 2021, MigMit wrote:
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?
What I'm after is documentation of n-ary functions. Suppose f :: a -> a -> Maybe a f arg1 arg2 = if arg1 < arg2 then Nothing else Just arg2 The docstring of f should be a function that, given descriptions of the arguments, generates a description of the result. E.g. doc_f = "if " <> arg1 <> " is smaller than " <> arg2 <> " then Nothing else Just " <> arg2 Say you have concrete arguments which are already tagged with a description: x :: (String,a) y :: (String,a) One could then have an operator <%> that acts like function application but at the same time takes care of documentation: func desc_f f <%> x <%> y :: (String,c) Here 'func' is an operator that translates the hypothetical docstring type into a real function. My provenience package currently burdens the user with constructing the docstrings by manually inserting the appropriate descriptions from x and y into doc_f. I'd like to automate that and make it more type-safe so that mismatch between documentation and type of f is a compile-time error. Olaf
On 3 Jun 2021, at 22:21, Olaf Klinke
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.

On Fri, 4 Jun 2021, Olaf Klinke wrote:
On Thu, 3 Jun 2021, MigMit wrote:
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?
What I'm after is documentation of n-ary functions. Suppose
f :: a -> a -> Maybe a f arg1 arg2 = if arg1 < arg2 then Nothing else Just arg2
The docstring of f should be a function that, given descriptions of the arguments, generates a description of the result. E.g.
doc_f = "if " <> arg1 <> " is smaller than " <> arg2 <> " then Nothing else Just " <> arg2
Say you have concrete arguments which are already tagged with a description: x :: (String,a) y :: (String,a)
One could then have an operator <%> that acts like function application but at the same time takes care of documentation:
func desc_f f <%> x <%> y :: (String,c)
Here 'func' is an operator that translates the hypothetical docstring type into a real function.
I don't fully understand the problem, but for me it sounds like an Applicative functor: data T a = Cons String a x,y :: T a func desc_f f <*> x <*> y :: T c
participants (3)
-
Henning Thielemann
-
MigMit
-
Olaf Klinke