Email Gateway (Aug 19 2022 at 17:27): Email Gateway (Aug 19 2022 at 17:27):From: Lars Hupel <hupel@in.tum.de>
Dear list,
I'd like to propose a new warning for the code generator. Very often,
additional class constraints get introduced. For example, virtually any
function on sets requires an 'equal' constraint. This is usually
expected. However, I was surprised when some set comprehensions
introduced 'enum' constraints:
definition "foo A = {x + 1|x. x ∈ A ∧ x > 5}"
export_code foo in Haskell
The generated code has the signature
foo ::
forall a.
(Enum.Enum a, Eq a, Arith.Numeral a,
Orderings.Ord a) => Set.Set a -> Set.Set a;
I can see why this is happening, but I only discovered it by manually
browsing through the generated code. Hence, a warning could be useful,
e.g. along the lines of:
'Generated code for foo has additional class constraints equal, enum'
Would anybody else consider that useful?
Cheers
Lars
Email Gateway (Aug 19 2022 at 17:31):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Lars,
unfortunately such additional constraints are quite pervasive, hence
such a warning would be so ubiquitous that users will just ignore it.
Generally, you can rely on nothing about the generated code except
partial correctness; so, inspection to find out what's going on cannot
be avoided at all.
Cheers,
Florian
signature.asc
Last updated: Apr 25 2024 at 08:20 UTC