<html><head><meta http-equiv="Content-Type" content="text/html charset=iso-8859-1"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div><div>Am 26.05.2014 um 14:28 schrieb Andrei Popescu <<a href="mailto:uuomul@yahoo.com">uuomul@yahoo.com</a>>:</div><br><blockquote type="cite"><div><div style="background-color: rgb(255, 255, 255); font-family: 'times new roman', 'new york', times, serif; font-size: 14pt; position: static; z-index: auto; "><div class="" style="font-size: 18.6667px; font-family: 'times new roman', 'new york', times, serif; background-color: transparent; font-style: normal; ">I have the following proposal:</div><div class="" style="font-size: 18.6667px; font-family: 'times new roman', 'new york', times, serif; background-color: transparent; font-style: normal; "><br></div><div class="" style="font-size: 18.6667px; font-family: 'times new roman', 'new york', times, serif; background-color: transparent; font-style: normal; ">(1) Hide all the extra structure from the user if it is not required explicitly.</div><div class="" style="font-size: 18.6667px; font-family: 'times new roman', 'new york', times, serif; background-color: transparent; font-style: normal; "><br></div><div class="" style="font-size: 18.6667px; font-family: 'times new roman', 'new york', times, serif; background-color: transparent; font-style: normal; ">(2) Make parts of this structure visible upon request by "get" commands that specify the target datatype and the desired <br></div><div class="" style="font-size: 18.6667px; font-family: 'times new roman', 'new york', times, serif; background-color: transparent; font-style: normal; ">components, which can be issued at any time (not necessarily immediately) after the datatype definition. Something like:</div><div class="" style="font-size: 18.6667px; font-family: 'times new roman', 'new york', times, serif; background-color: transparent; font-style: normal; "><br></div><div class="" style="font-size: 18.6667px; font-family: 'times new roman', 'new york', times, serif; background-color: transparent; font-style: normal; ">datatype 'a list = Nil | Cons 'a "'a list"</div><div class="" style="font-size: 18.6667px; font-family: 'times new roman', 'new york', times, serif; background-color: transparent; font-style: normal; "><br></div><div class="" style="font-size: 18.6667px; font-family: 'times new roman', 'new york', times, serif; background-color: transparent; font-style: normal; ">...</div><div class="" style="font-size: 18.6667px; font-family: 'times new roman', 'new york', times, serif; background-color: transparent; font-style: normal; "><br></div><div class="" style="font-size: 18.6667px; font-family: 'times new roman', 'new york', times, serif; background-color: transparent; font-style: normal; ">getSelector isNil for Nil[list]</div><div class="" style="font-size: 18.6667px; font-family: 'times new roman', 'new york', times, serif; background-color: transparent; font-style: normal; "><br></div><div class="" style="font-size: 18.6667px; font-family: 'times new roman', 'new york', times, serif; background-color: transparent; font-style: normal; ">Then novices will first get a chance to experiment with defining their own selectors, set, map, etc. before they are shown <br></div><div class="" style="font-size: 18.6667px; font-family: 'times new roman', 'new york', times, serif; background-color: transparent; font-style: normal; ">how to get them for free. <br></div></div></div></blockquote><div><br></div></div>Do I understand you correctly that you are volunteering to implement this?? I wish you good luck, to derive theorems like "sel_map" etc. on a per-need basis. It's certainly doable, but would be an architectural nightmare.<div><br></div><div>Seriously: We've had a discussion after lunch. We haven't agreed on a concrete syntax, but some elements have emerged:</div><div><br></div><div>1. The squiggles (-: and =:) are easy to get rid of, and we'll kill them. This has been discussed before.</div><div><br></div><div>2. We'll try to move (map: ... rel: ...) out of the way, e.g. by putting them after the definition rather than before.</div><div><br></div><div>3. Similar story for the set function (set: 'a), even though it's a bit painful in the general case (with, say, ten type variables and five mutually recursive types -- cf. IsaFoR).</div><div><br></div><div>4. The selector syntax seems acceptable to most of not all parties. Some of us even love it. Also important is that readers are usually smart enough to infer, from the names of the things, what is meant (e.g. "hd" and "tl" for a list have to be the selectors).</div><div><br></div><div>5. The discriminators are a bit more iffy, and could perhaps be labeled more clearly, e.g. with a pseudo-keyword "discriminator". On the other hand, they're not needed for "list" and "option", and the default name (is_C for constructor C) is good.</div><div><br></div><div>6. The default values for, e.g. "tl [] = []", could be specified as equations after the definition (e.g. in a "where" clause), as suggested one year ago by Andreas L.</div><div><br></div><div>One scheme that appeared promising as a compromise is to specify replacement names at the end of the definition, e.g.</div><div><br></div><div> with</div><div> map := map_list</div><div> set := set_list</div><div> list_all2 := rel (* ugly name BTW -- maybe*)</div><div><br></div><div>This scales gracefully to the mutual case.</div><div><br></div><div>I'll do step 1 now, and we can give ourselves more time to think about 2 to 6.</div><div><br></div><div>Jasmin</div><div><br></div></body></html>