On Monday, 25 August 2014 20:14:01 UTC+2, Robert Bradshaw wrote:
>
> On Mon, Aug 25, 2014 at 6:02 AM, Bill Hart <goodwi...@googlemail.com
> <javascript:>> wrote:
> > Hmm. Some more explaining is necessary.
> >
> >
> > On Monday, 25 August 2014 12:04:16 UTC+2, Pierre wrote:
> >>
> >> Thanks again for the explanations. I realize that there were many
> things
> >> about Julia/Nemo which I had misunderstood. Let me explain a little, so
> I
> >> can (i) embarrass myself a little more, and (ii) perhaps give an
> indication
> >> of common mistakes, for anyone who would write a tutorial about
> Julia/Nemo
> >> :-)
> >>
> >> Mistake (1): taking it for OOP.
> >
> >
> > Julia is OOP!
> >
> > There are two ways to do OOP. The first is with classes and usually
> single
> > dispatch and the other is with multi-methods. The latter is the Julia
> way
> > and it is more flexible.
> >
> > There is a dual notion for data structures as well, and Julia supports
> that
> > too, giving even greater flexibility. The combination of the two is more
> > powerful than standard OOP, which can be very restrictive in practice.
> >
> >>
> >> When hearing about the way Julia worked, I jumped when I saw it wasn't
> OO,
> >> and then naturally was looking for ways to emulate OOP with Julia
> (rather
> >> than make the effort of a paradigm shift). And with multi-dispatch, i
> >> thought OK, if I want to write code that applies to objects of type A,
> B and
> >> C at once, just declare them A <: X, B <: X and C <: X and define f(x
> :: X).
> >> However this gave me the wrong intuition " A <: X is the same as A
> inherits
> >> from X".
> >
> >
> > None of that makes sense.
> >
> > f(x :: X) is the way you write a function prototype in Julia. It
> corresponds
> > to the following prototype in C.
> >
> > void f(X x);
> >
> > X is just a type, like int or float or double or MyType, etc. In Julia,
> you
> > just write the type on the right, after a double colon, instead of on
> the
> > left like C.
> >
> > A <: X does not mean A is an object of type X. It means A is a subtype
> of X,
> > where both A and X are types (one or both may be abstract types).
> >
> > The way to write "A is an object of type X" is A :: X.
> >
> > The way to write "X is a subtype of Y" is X <: Y.
> >
> > But remember that subtype here *may* mean X is in the typeclass Y.
> >
> >>
> >> At this point, the fact that abstract types could be instantiated was
> seen
> >> as a limitation compared to OOP.
> >
> >
> > No. There is no similar concept in OOP, except for languages like scala
> > which have traits/interfaces/typeclasses. It's an extension over and
> above
> > what is found in standard OOP languages.
> >
> > You can also write all your Julia programs without any <: symbols if you
> > want. And in fact you can leave all types out too and let Julia figure
> them
> > out.
> >
> > Types and subtyping simply allows you to restrict what is allowed.
> Otherwise
> > everything is allowed, just like Python.
> >
> >>
> >> And somehow, it is.
> >
> >
> > No it is not. You never need to use the <: notation in Julia if you
> don't
> > want to. You can just stick to values (objects) and types (classes) if
> you
> > want. Then you have the same thing as standard OOP. You can even
> restrict
> > yourself to single dispatch if you want, in which case you have OOP
> exactly.
> > But there's no reason to restrict yourself in this way, because Julia
> offers
> > all the other goodies on top of that.
> >
> >>
> >> Except at the same time, the type system does many new things. Apples
> and
> >> oranges, really.
> >>
> >> Mistake (2): taking types for sets.
> >
> >
> > They sort of are. Formally a type is just a set of values. Well, not in
> a
> > mathematical sense. But in some intuitive sense.
> >
> > Types of course satisfy some calculus just as sets do and the rules of
> the
> > calculus are somewhat similar, but not quite the same. Technically
> dependent
> > types correspond exactly to predicates in the predicate logic, via Type
> > theory (an extension of the Curry-Howard isomorphism). But that's all a
> bit
> > complicated, so we informally think of types as sets.
> >
> > One big difference is there are plenty of non-computable functions
> between
> > sets. But the functions between types are always computable. But again,
> it's
> > not even vaguely necessary to understand this to get the concept of a
> type.
> > It's intuitively just a name given to the collection of all values which
> an
> > object of that type can have.
> >
> >> This little discussion about names reveals another mistake of mine:
> >> thinking of types as sets. I thought ZZ <: QQ for example.
> >
> >
> > Yeah, the <: notation doesn't mean contained in. It's not a mathematical
> > operator. It means "subtype of". There are three things the notation can
> > mean:
> >
> > 1) If A <: B where A and B are types, then it means that if a function
> can
> > take an argument of type B, then an argument of type A will work just as
> > well in its place. In some sense, the set of values of type A is a
> > restriction of the set of values of type B. This is pretty close to a
> subset
> > meaning though technically it has more to do with the representation in
> bits
> > on the machine than anything mathematical.
> >
> > 2) If A <: B where A is a type and B is an abstract
> > type/typeclass/interface/trait, it means that a function which requires
> a
> > type in class B can take the type A. This is not a subset meaning. It
> means
> > the type A belongs to the typeclass B.
> >
> > 3) If A <: B where A and B are both abstract
> > types/typeclasses/interfaces/traits, it means that a function which
> requires
> > a type in class B can take a type in class A. This is a essentially a
> subset
> > meaning, but the sets here are sets of types, not sets of values as in
> (1).
> >
> > There aren't many examples of (1) in Julia that I can think of. Trivial
> ones
> > such as Int <: Int are the only ones that come to mind. I really can't
> think
> > of any other examples.
> >
> > In fact, I think it is a general principle in Julia that concrete types
> > cannot subtype one another. This isn't the case in some other languages,
> but
> > it is the case in Julia. So (1) above essentially never happens, except
> for
> > T <: T for concrete types T.
> >
> > This is maybe an oddity, but it's not a restriction. You can still cast
> > between types to your heart's content.
> >
> >> That's not even consistent with the previous mistake. In Sage say, i'm
> >> guessing QQ is of type Field or something, which inherits from a type
> Ring
> >> or something -- but not the other way around!
> >
> >
> > Yeah in Julia you'd have QQ <: Field <: Ring.
> >
> > The first <: in that is of sort (2) above. The second <: is of sort (3).
> >
> >> So mistake (1) should have led me to believe QQ <: ZZ. Oh well.
> >
> >
> > We have neither QQ <: ZZ nor ZZ <: QQ. Both are concrete types and may
> not
> > subtype each other. This is not essential, and in fact is not the case
> in
> > some other languages. But it is the case in Julia.
> >
> >>
> >>
> >> Mistake (3): thinking about Sage too much. To my discharge, ZZ in Sage
> is
> >> an object,
> >
> >
> > Correct. But classes are essentially objects in Python because
> everything is
> > an object, pretty much. This really muddies the water. Better to think
> of
> > classes and objects as being separate concepts.
>
> I, for one, find it very convenient (especially compared to using
> reflection and other hacks that are needed to reason about type at
> runtime in C++ or Java). Not that some languages aren't even better.
>
> > Also better to think of ZZ as a class in Sage and elements of ZZ as
> objects,
> > even though actually ZZ happens to be an object too because Python.
>
> No. ZZ is an object because you might want to do things with it, like
> ask for it's properties (is it infinite?)
Sorry if I have that wrong. But when I type ZZ?? into Sage, it pulls up the
definition of a class.
Anyway, it's irrelevant because Python.
In Julia types are also able to be passed around as first class objects.
Which means you can define multimethods which take types as parameters. I
do this all the time in Nemo.
So I can send a type to a function which gives me some properties of the
type, if I so wish. I thought about adding properties like is_infinite to
types in Nemo. But I found that I had been thinking the wrong way about
things all along.
> or use it as a parameter
> (e.g. the domain of a Map object). Sometimes the Objects (in the
> categorical sense) are more interesting than their elements.
>
If you are a category theorist yes. Most mathematicians think categories
are just sets.
>
> If your Objects are parameterized types,
I'm curious how you handle in
> Julia the fact that R[x] is a Euclidean domain iff R is a field.
I'm curious, is the category of Euclidean domains a full subcategory of
Rings?
> (As
> you mention, trying to use the type hierarchy in Python to model
> categorical relationships in Sage has generally lead to pain which is
> why we're moving away from that...)
>
Oh I can't think why.
>
> > Roughly speaking a Julia value has some similarity to a Python object
> and a
> > Julia type has some similarity to a Python class. That's a very
> misleading
> > identification, but there is some truth to it.
> >
> > Sage is a different beast to Python. As I mentioned, ZZ is not meant to
> be
> > either an object or a class. It is meant to be a mathematical domain.
> And
> > mathematical domains are being *modeled* in Python using classes, (which
> > just happen to be objects in Python for the LOL's). That's of course a
> > bastardisation of all that is good and pure. But both identifications
> occur
> > for somewhat valid reasons.
> >
> > Classes are objects in Python so that you can do things to classes just
> as
> > you would any object in the language. The official reason is so that you
> can
> > rename and import classes. But I rather think there's more to it than
> that.
> >
> > And mathematical domains in Sage are modeled as classes because that is
> the
> > most convenient thing in Python to model them with. Unlike Aldor, Python
> > doesn't have a native domain or category concept. So you have to pick
> > something that works well enough.
> >
> > It is worth noting that mathematical categories cannot in general be
> modeled
> > accurately with computer science types. There's a fundamental mismatch
> > between category theory and types. This has led some mathematicians to
> > completely redo the foundations of mathematics in terms of homotopy
> classes
> > instead of category theory. And this can be modeled accurately in terms
> of
> > Martin-L\"{o}f Type theory. This new foundation for mathematics is
> called
> > the Univalent Foundation for Mathematics, and was developed primarily by
> > Vladimir Veovodsky based on the Type theory of Per Martin-L\"{o}f.
> >
> > I would suggest that a good dependent type system is just as good as a
> > Martin-L\"{o}f Type Theory any day. So for most practical purposes we
> can
> > model mathematics reasonably well with dependent types. We can't quite
> push
> > the carpet down at the edges. But we can get most of the wrinkles out.
> >
> > Sage attempts to model a dependent type system using classes in Python.
> I
> > won't start a huge digression into the manifold problems with this
> approach.
> > But it involves a lot of work, for one thing.
> >
> >> like 1/2, not a type or anything.
> >
> >
> > It's better to think of it as a type or class if you want to think of it
> as
> > anything computational. It happens to be an object too. But that is an
> > accident forced on you by Smalltalk, err I mean Python.
> >
> >>
> >> This has unconsciously contributed to my confusion greatly. Also the
> fact
> >> that there is a coercion from ZZ to QQ, and somewhere I must have taken
> A <:
> >> B to mean "there is a coercion from A to B".
> >
> >
> > Ah, no. Coercion is another thing entirely. That is primarily a
> mathematical
> > concept. Though there is a related computer science concept called
> > conversion and promotion which has nothing to do with the mathematical
> > concept of coercion, but which is the nearest related concept.
> >
> > Mathematical coercion is a myth. There is no consistent formal
> foundation
> > for coercion whatsoever.
> >
> > The mathematical concept of coercion is nothing more than a bunch of
> > incompatible and inconsistent informal notions that mathematicians carry
> > around in their collective heads to relate the informal, inconsistent
> and
> > incompatible definitions the carry around in their heads.
> >
> > Any formal and consistent axiomatisation of computer algebra will
> deviate
> > arbitrarily far from what any given mathematician thinks is reasonable.
> >
> > Anyway, best to think of A <: B as meaning A is a subtype of B, where in
> > Julia at least B needs to be an abstract type, except in the trivial A
> <: A
> > case.
> >
> > In a sense, you do want to have coercions from types in class A to types
> in
> > class B where A <: B, usually. But it is much more subtle than that,
> > especially in Julia where types can be parametric. Even if A <: B you
> don't
> > automatically have T{A} <: T{B} in Julia. This would be called a
> covariant
> > type system, whereas Julia is invariant.
> >
> > So even if you had ZZ <: QQ in Julia (which you don't), you wouldn't
> > automatically have Poly{ZZ} <: Poly{QQ}. And even if you did, that would
> > have nothing to do with conversions and promotions because the
> conversion
> > and promotion system can have arbitrary types in Julia and is completely
> > decoupled from the subtyping system.
> >
> > Decoupling is good because it gives you more flexibility to do whatever
> you
> > want to do. You give your own meaning to things, and you only define the
> > promotions and conversions you want.
> >
> > Bill.
> >>
> >>
> >> Pierre
> >>
> >>
> >>
> >>
> >>
> >>>
> > --
> > You received this message because you are subscribed to the Google
> Groups
> > "sage-devel" group.
> > To unsubscribe from this group and stop receiving emails from it, send
> an
> > email to sage-devel+...@googlegroups.com <javascript:>.
> > To post to this group, send email to sage-...@googlegroups.com
> <javascript:>.
> > Visit this group at http://groups.google.com/group/sage-devel.
> > For more options, visit https://groups.google.com/d/optout.
>
--
You received this message because you are subscribed to the Google Groups
"sage-devel" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to sage-devel+unsubscr...@googlegroups.com.
To post to this group, send email to sage-devel@googlegroups.com.
Visit this group at http://groups.google.com/group/sage-devel.
For more options, visit https://groups.google.com/d/optout.
