Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-03-07

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

Time Nick Message
07:33 JCaesar oO. The definition of ≤ on string is weird…
07:56 ThreeOfEight What do you mean? "string" is not a type
07:56 ThreeOfEight I mean, not a defined type
07:57 ThreeOfEight it's just a synonym for char list
07:57 ThreeOfEight so the definition of "<=" on string is just the definition of "<=" on lists
07:57 JCaesar Hm.
07:58 JCaesar makes me wonder why an 'a list is not a linorder, if 'a is a linorder… or am I overlooking something here?
07:58 ThreeOfEight there is the String.literal type
07:59 ThreeOfEight well, the problem is, there are several ways you could define this
07:59 ThreeOfEight the most obvious one is lexicographic ordering
07:59 ThreeOfEight ~~/src/HOL/Library/List_lexord provides that
08:00 ThreeOfEight if you import "~~/src/HOL/Library/List_lexord" and "~~/src/HOL/Library/Char_ord", you get lexicographic ordering on strings
08:01 ThreeOfEight note that when exporting code, you should not work with strings, but with String.literal
08:01 ThreeOfEight because String.literal gets mapped to target-language strings
08:01 ThreeOfEight whereas string is just char list, and will therefore be mapped to lists of characters in the target language
08:02 JCaesar That is important information.
08:02 ThreeOfEight in Haskell, there's no difference (although one could map string to Text in that case), but in ML and OCaml and Scala, there is.
08:02 JCaesar Wait, what? At least I got lists of nibbles last time I exported strings to Haskell…
08:02 ThreeOfEight Yes, you have to import Code_Char for that.
08:03 JCaesar And… oh. String.literal also has no linorder defined… that doesn't happen to be done somwhere already?
08:03 ThreeOfEight that maps Isabelle's Chars to target-language characters
08:03 JCaesar Magic. :)
08:03 ThreeOfEight well you can tell the code generator to map certain Isabelle constants to target-language constants
08:04 ThreeOfEight which is pretty dangerous, but the code generator experts generally know what they're doing
08:04 JCaesar Which is exactly my definition of magic.
08:04 ThreeOfEight and by "code generator experts", I mean "Florian Haftmann"
08:04 ThreeOfEight it doesn't seem like there is any definition of linear orderings on String.literal, no
08:05 ThreeOfEight if you need that: write to the mailing list and suggest it
08:05 ThreeOfEight one would have to be careful to see what the comparison operators do on native strings in the target languages
08:06 ThreeOfEight but lexicographic ordering is pretty much the only thing that makes sense
08:19 JCaesar Hmm. Char_ord seems to provide an ordering. (At least I have no other explanation why this suddenly works.)
08:31 ThreeOfEight yes, it provides an ordering for char
08:32 ThreeOfEight oh!
08:32 ThreeOfEight and also one for String.literal
08:32 ThreeOfEight yes
08:32 ThreeOfEight my mistake was to grep for "instantiation literal"
08:32 ThreeOfEight I should have grepped for "String.literal"
08:32 ThreeOfEight (there's a "hide_type (open) literal" there
12:41 dmiles joined #isabelle
13:01 larsrh joined #isabelle
15:25 dmiles joined #isabelle
16:06 dmiles joined #isabelle
19:52 wagle joined #isabelle

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary