Re: [isabelle] Problems with linear orders and strings



2011/3/4 Peter Lammich <peter.lammich at uni-muenster.de>

>
> > Peter, can you remove the pair-ordering in common/Misc and load
> Product_ord instead (it is the same definition)?
> >
>
> If it is the same definition, and Product_ord is in the Isabelle
> standard library, it should of course be changed to avoid duplication
> and clashes!
>  @Rene: For the first time, you should change it in your local copy. If
> you are using the stable version, there is no other way.
>     For the development version, someone (probably me or some of the
> afp maintainers) should setup a development snapshot, do the change,
> test if nothing breaks, and push it into the hg-repository.
>
> Otherwise, it highlights some general problem with type classes:
>  If there is more than one way to say order a datatype, which one
> should go into the typeclass.
>  I think there is such a problem for multisets, where there are two
> orderings that are both "the natural" one when viewed from the right
> perspective.
>  And, if formalizations get large, there may be parts where one order
> is the "natural" one, and other parts where the other order is the
> "natural" one, and
>  then things seems to clash ...
>

Can't help but comment on this... there are alternative designs for
type classes in which instance declarations are lexically scoped.
This allows different instance declarations to be in effect for different
scopes.

@inproceedings{Siek:2005:ELS:1065010.1065021,
 author = {Siek, Jeremy G. and Lumsdaine, Andrew},
 title = {Essential language support for generic programming},
 booktitle = {Proceedings of the 2005 ACM SIGPLAN conference on
Programming language design and implementation},
 series = {PLDI '05},
 year = {2005},
 isbn = {1-59593-056-6},
 location = {Chicago, IL, USA},
 pages = {73--84},
 numpages = {12},
 url = {http://doi.acm.org/10.1145/1065010.1065021},
 doi = {http://doi.acm.org/10.1145/1065010.1065021},
 acmid = {1065021},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {C++, Haskell, generic programming, polymorphism, standard ML},


}

@inproceedings{Dreyer:2007:MTC:1190216.1190229,
 author = {Dreyer, Derek and Harper, Robert and Chakravarty, Manuel M.
T. and Keller, Gabriele},
 title = {Modular type classes},
 booktitle = {Proceedings of the 34th annual ACM SIGPLAN-SIGACT
symposium on Principles of programming languages},
 series = {POPL '07},
 year = {2007},
 isbn = {1-59593-575-4},
 location = {Nice, France},
 pages = {63--70},
 numpages = {8},
 url = {http://doi.acm.org/10.1145/1190216.1190229},
 doi = {http://doi.acm.org/10.1145/1190216.1190229},
 acmid = {1190229},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {modules, type classes, type inference, type systems},
}

Cheers,
Jeremy


>
> Unfortunately, the ICF interfaces are currently not parameterizable by
> the used order, hash-function, equality-operator, ...
>  @Andreas: What was the state of discussion there, is it possible/worth
> the effort to parameterize?
>
> Best,
>  Peter
>
>
> > I have the following workaround, but of course this should be fixed in a
> better way.
> >
> > theory Linorders
> > imports List_lexord Char_nat (* but not Char_prod *)
> > begin
> >
> > instantiation char :: linorder
> > begin
> > fun less_eq_char :: "char \<Rightarrow> char \<Rightarrow> bool" where
> "less_eq_char c d = (nat_of_char c \<le> nat_of_char d)"
> > fun less_char :: "char \<Rightarrow> char \<Rightarrow> bool" where
> "less_char c d = (nat_of_char c < nat_of_char d)"
> >
> > instance
> > proof
> >   fix x y :: char
> >   assume "x \<le> y" and "y \<le> x"
> >   hence "nat_of_char x = nat_of_char y" (is "?x = ?y") by auto
> >   hence "char_of_nat ?x = char_of_nat ?y" by simp
> >   thus "x = y" unfolding char_of_nat_of_char .
> > qed auto
> > end
> >
> > Afterwards strings are in class linorder, code-generation works also
> after Code_Char_chr,
> > and I can use RBTMapImpl as there is no conflict between Misc and
> Product_ord.
> >
> > Cheers,
> > René
> >
>
>
>


-- 
____________________________________
Jeremy Siek <jeremy.siek at colorado.edu>
http://ecee.colorado.edu/~siek/
Assistant Professor
Dept. of Electrical, Computer, and Energy Engineering
University of Colorado at Boulder




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