Re: [fricas-devel] [PATCH] None is the top type, fix documentation
On Thu, Jun 14, 2018 at 2:54 AM, Waldek Hebisch 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 fricas-devel+unsubscr...@googlegroups.com. To post to this group, send email to fricas-devel@googlegroups.com. Visit this group at https://groups.google.com/group/fricas-devel. For more options, visit https://groups.google.com/d/optout.
Re: [fricas-devel] [PATCH] Void is the unit type, fix doc and cleanup (use 0 as representation)
> However I am uncertain about your proposed changes to Void. Why do you > prefer a value of 0 instead of the symbol "()"? Note of course that > this is a Lisp symbol and not Lisp NIL. Although the value can be > anything, as the empty tuple, I think () is more intuitive than 0. A > value of 0 might be a bit confusing since the unit *type* is usually > denoted by 1, not 0. I see no harm in letting the Rep for Void be > String. In fact why not just define > > void() == "()" The underlying value of Void is not important, because the type Void can only have one possible value. I don't want to use string because of possible memory waste. > Is the Lisp function call voidValue really important for some reason > like in-line optimization? 'voidValue' is used a few places in the compiler. > Also, why did you make the following changes in Exit? > > -coerce(n:%) == error "Cannot use an Exit value." > -n1 = n2 == error "Cannot use an Exit value." Because Exit is the bottom type, no variable can have an Exit value, therefore, it can't be printed or compared. When encountering Exit type, the function aborts. > From a formal point of view I am not certain at all about None. Since > FriCAS is a statically typed language I think it would be nice if None > could be eliminated from the library. FriCAS already has the type Any > which implements a type-correct version of "duck typing" and plays the > role of a universal type. None as the top type is very necessary. The difference between Any and None is that Any contains the value and type, None just contains the value. None is widely used and can't be replaced. Although I think "None" is a terrible name. -- 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 fricas-devel+unsubscr...@googlegroups.com. To post to this group, send email to fricas-devel@googlegroups.com. Visit this group at https://groups.google.com/group/fricas-devel. For more options, visit https://groups.google.com/d/optout.
Re: [fricas-devel] [PATCH] inline optimize 'powmod'
> > This patch can speed up function call 'primes(1, 10^7);' > by 20%. OK. > diff --git a/src/algebra/integer.spad b/src/algebra/integer.spad > index a5689694..924ba6db 100644 > --- a/src/algebra/integer.spad > +++ b/src/algebra/integer.spad > @@ -183,6 +183,18 @@ > --TT := InnerModularGcd(%, ZP, 67108859 pretend %, myNextPrime) > --gcdPolynomial(p, q) == modularGcd(p, q)$TT > > + -- copied from IntegerNumberSystem to get inline optimization, > + -- speeds up functions like 'primes' > + powmod(x, n, p) == > + if negative? x then x := positiveRemainder(x, p) > + zero? x => 0 > + zero? n => 1 > + y : % := 1 > + z := x > + repeat > +if odd? n then y := mulmod(y, z, p) > +zero?(n := shift(n, -1)) => return y > +z := mulmod(z, z, p) > > )abbrev domain NNI NonNegativeInteger > ++ Author: > > -- > 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 fricas-devel+unsubscr...@googlegroups.com. > To post to this group, send email to fricas-devel@googlegroups.com. > Visit this group at https://groups.google.com/group/fricas-devel. > For more options, visit https://groups.google.com/d/optout. > -- Waldek Hebisch -- 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 fricas-devel+unsubscr...@googlegroups.com. To post to this group, send email to fricas-devel@googlegroups.com. Visit this group at https://groups.google.com/group/fricas-devel. For more options, visit https://groups.google.com/d/optout.
Re: [fricas-devel] [PATCH] None is the top type, fix documentation
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. 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. -- Waldek Hebisch -- 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 fricas-devel+unsubscr...@googlegroups.com. To post to this group, send email to fricas-devel@googlegroups.com. Visit this group at https://groups.google.com/group/fricas-devel. For more options, visit https://groups.google.com/d/optout.
Re: [fricas-devel] [PATCH] Void is the unit type, fix doc and cleanup (use 0 as representation)
On Tue, Jun 12, 2018 at 9:37 AM, oldk1331 wrote: > Clearly domain "Void" is the unit type: > https://en.wikipedia.org/wiki/Unit_type > > So I'm clearing this up. > I think that fixes and better documentation of the Void, Exit, and None domains are quite welcome but still warrant some discussion. From a formal linguistic or categorical point of view Void (terminal object) and Exit (initial object) are more important than they look. As a category, FriCAS domains should form at least a Cartesian category (although I think an even better model might be a topos). However I am uncertain about your proposed changes to Void. Why do you prefer a value of 0 instead of the symbol "()"? Note of course that this is a Lisp symbol and not Lisp NIL. Although the value can be anything, as the empty tuple, I think () is more intuitive than 0. A value of 0 might be a bit confusing since the unit *type* is usually denoted by 1, not 0. I see no harm in letting the Rep for Void be String. In fact why not just define void() == "()" Is the Lisp function call voidValue really important for some reason like in-line optimization? Also, why did you make the following changes in Exit? -coerce(n:%) == error "Cannot use an Exit value." -n1 = n2 == error "Cannot use an Exit value." >From a formal point of view I am not certain at all about None. Since FriCAS is a statically typed language I think it would be nice if None could be eliminated from the library. FriCAS already has the type Any which implements a type-correct version of "duck typing" and plays the role of a universal type. -- 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 fricas-devel+unsubscr...@googlegroups.com. To post to this group, send email to fricas-devel@googlegroups.com. Visit this group at https://groups.google.com/group/fricas-devel. For more options, visit https://groups.google.com/d/optout.
