On Thu, Jun 14, 2018 at 2:54 AM, Waldek Hebisch <[email protected]> wrote: > oldk1331 wrote: >> >> Domain "None" is the top type in type theory: >> >> https://en.wikipedia.org/wiki/Top_type >> > > We had discussions about None, Void and probably also Exit in > the past. People have nice ideas how to cleanly integrate > them into type system. But the botton line is: None is really > a big hole in type system, breaking normal rules. Exit > and to same degree Void are hardwired into compiler to > get specific functionality. Claiming clean semantics of > those types with current compiler is more or less misleading.
Yes, because None/Void/Exit have specials places in type theory, they are hard coded into compiler. We should recognize this. (Exit is related with error handling, Void is related with one-arm-if, None is related with coercion.) I have follow up commits that improve the compiler bits that deals with None/Void/Exit. > I do not see why you want to change code here: the types are > closely tied to compiler and seem to contain what is needed > (and probably nothing more). Trying to change them risks > obscure bugs. Any change there requires serious analysis > of effects. I'm only modifying the Spad part right now, and mostly removing signatures that no one uses. These changes are safe. -- You received this message because you are subscribed to the Google Groups "FriCAS - computer algebra system" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To post to this group, send email to [email protected]. Visit this group at https://groups.google.com/group/fricas-devel. For more options, visit https://groups.google.com/d/optout.
