Email Gateway (Aug 22 2022 at 11:27): Email Gateway (Aug 22 2022 at 11:27):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
I am currently thinking about introducing a type 'a egf for exponential
generating functions, derived from formal power series ('a fps).
I was wondering how to best express the n-th coefficient of an egf. For
polynomials, only the rather unwieldy notation "coeff f n" exists. For
formal power series, "f $ n" exists.
I considered overloading the $ notation so that it works for
polynomials, formal power series, and exponential generating functions.
However:
– introducing a typeclass does not work, because this would be a
higher-order typeclass.
– Vanilla ‘overloading’ works, but the type of "op $" must then be 'a ⇒
nat ⇒ 'b, which means that type inference cannot deduce the result type
of "f $ 0" even when the type of "f" is known, requiring type
annotations everywhere.
– Adhoc overloading would probably work, but that is somewhat… ad-hoc.
Does anybody have other ideas?
Manuel
Email Gateway (Aug 22 2022 at 11:27):From: Johannes Hölzl <hoelzl@in.tum.de>
Hm, I think the usual option is to just go with a new $ notation. Maybe
using context/private notation tricks?
Alternatively, you could also try to use the coercion from 'a egf to 'a
fps, and then introduce a output abbreviation:
f $_fps x == fps_of_egf f $ x
Last updated: Apr 25 2024 at 04:18 UTC