Stream: Beginner Questions

Topic: Coercion inference rat

Salvatore Francesco Rossetta (Dec 07 2023 at 11:35):

Hi, I have this code

definition update_votes :: "'a ⇒ 'a Seats ⇒ 'a StructVotes ⇒ 'a StructVotes ⇒ nat list ⇒ 'a StructVotes" where
"update_votes party tot_seats votes fract_votes params ≡
  let
    ns::nat = count_seats party tot_seats (length params);
    p::nat = List.nth params ns;
    v::rat = votes party;
    updated_fract_votes :: 'a StructVotes = fract_votes(party := v / rat_of_nat p)
  in
    updated_fract_votes
  end"

shortly, i retrieve the number of seats of input party 'a, take parameter from input nat list, perform a division and update another function called fract_votes. it should return a 'a StructVotes, which is

type_synonym 'a StructVotes = "'a ⇒ rat"

But the code gives me a coercion error

Type unification failed: Clash of types "rat" and "_ ⇒ _"

Type error in application: incompatible operand type

Operator:  (≡) (update_votes party tot_seats votes fract_votes params) :: ('a ⇒ rat) ⇒ prop
Operand:
  let ns = count_seats party tot_seats (length params); p = params ! ns; v = votes party;
      updated_fract_votes = fract_votes(party := v / rat_of_nat p)
  in updated_fract_votes end ::
  rat

Coercion Inference:

Local coercion insertion on the operand failed:
No coercion known for type constructors: "rat" and "fun"

but I can't understand why: I think it's about the output of the function but i wrote it to be 'a StructVotes and if I am returning updated_fract_votes shouldn't it be a 'a StructVotes?

also i think that "fract_votes(party := v / rat_of_nat p)" is only adding another correspondence between party and a number and not actually overwriting the already existing one, which is my aim, but this is another problem that I can fix later since it's logic and not syntax.

Salvatore Francesco Rossetta (Dec 07 2023 at 12:22):

Nevermind this question, in the end I solved it , really stupid error: had to remove the "end" at the end of the definition.

Manuel Eberl (Dec 07 2023 at 12:45):

Any reason why you're using rational numbers and not real numbers?

Manuel Eberl (Dec 07 2023 at 12:45):

Just as an observation it's kind of rare for people to explicitly use the "rat" type for anything. But if you really want only rational numbers then that is of course the way to go.

Wolfgang Jeltsch (Dec 07 2023 at 18:49):

I’d say that if you only encounter rational numbers then use the type for rational numbers. It’s kind of a pity that people, once they’ve learned about real numbers in school, always use the hammer (real numbers), even when some more specific tool (rational numbers) would be the more appropriate approach.

Salvatore Francesco Rossetta (Dec 08 2023 at 08:50):

Manuel Eberl said:

Just as an observation it's kind of rare for people to explicitly use the "rat" type for anything. But if you really want only rational numbers then that is of course the way to go.

Yes, rationals suit better my case because I only have to compare them and find the max value, so I can avoid using real numbers.

Last updated: Apr 28 2024 at 12:28 UTC