Re: [isabelle] Want a type of non-negatives for a field, to work like nat/int



Am 10.02.2014 14:38, schrieb Gottfried Barrow:
On 2/9/2014 4:40 PM, Ondřej Kunčar wrote:
On 02/09/2014 05:28 PM, Gottfried Barrow wrote:
(*NOTE: The "exception TYPE raised" error shown below might be of
interest to someone.)

For example me. Your type definition uses as a raw type a type variable. The new code in lifting that deals with parametricity assumes that the raw type is always a type constructor. I'll take a look at it.

Ondrej,

Thanks. I use `'a::linordered_idom option` as a workaround, as shown below.

NOTE for anyone: I can't get subtype coercion in the Rep direction, as show below. If someone can tell me whether I can or can't do that, I'd appreciate it.
Hi Gottfried,

there are two different algorithms in charge of inserting coercions:

(1) A complete (=if a term can be coerced it will be coerced) for structural subtyping (a.k.a. global coercion insertion in error messages), where only coercions between base types (i.e., nullary type constructors such as nat, int, real) are allowed. Map functions are used to lift those coercions between base types to more complex types (e.g, nat list or int option). In this "structural" setting, there might be a coercion from "nat list" to "int list" (given a coercion from nat to int and a map function for list), but never a coercion from "nat list" to "int option".

(2) An incomplete (Coq-style) algorithm for non-structual coercions (e.g. one from "nat list" to "int option"). This is called local coercion insertion in error messages.



typedef ('a::linordered_idom) loidOpt = "{x::'a option. x ~= None & the x >= 0}"
  by(auto)

(* The Rep declares don't return an error, but have no affect on coercions. *)
(*
declare [[coercion Rep_loidOpt]]
declare [[coercion "Rep_loidOpt::rat loidOpt => rat option"]]

term "(x::rat loidOpt) = Some (y::rat)"
*)

This is out of scope for (1). The incompleteness of (2) is visible on your example, which only will not insert coercions in the first argument of equality (and of other polymorphic functions). It would have worked if you had reversed the equation:

term " Some (y::rat) = (x::rat loidOpt)"

Dmitriy




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.