Julia, big data, HPC, critical applications and Katie Bouman's black hole?

#21

The only reason I mention it is purely due to my interest in the mathematics of it, I recommend looking at the referenced paper Engineering Proof by Reflection in Agda

Abstract. This paper explores the recent addition to Agda enabling reflection, in the style of Lisp and Template Haskell. It gives a brief introduction to using reflection, and details the complexities encountered when automating certain proofs with proof by reflection. It presents a library that can be used for automatically quoting a class of concrete Agda terms to a non-dependent, user-defined inductive data type, alleviating some of the burden a programmer faces when using reflection in a practical setting.

what does @jeff.bezanson have to say about it with respect to Julia?

0 Likes

#22

Has any “real world” safety critical system been developed using Haskell, Agda, Idris, or the like?

I suspect there’s a bit of a mismatch between what academic PL theorists like to work on and what is actually needed and desired. If this were not the case, there probably would have been no need for Julia, since Haskell was already there, and has some scientific computing libraries.

0 Likes

#23

Right, there has been some long standing discussion about adding some kind of explicit interface mechanism to Julia. @StefanKarpinski briefly describes the expected behavior of the feature, if it should ever make it into Julia

I’m all on board with that description!

1 Like

#24

When I think about it, I am not sure this is something that is either feasible or desirable.

Many of the implicit interfaces in Base are currently not even documented, or even generally recognized as interfaces despite the fact that people treat them as such. Very few package authors document interfaces, which suggests that doing so is burdensome. So what we have is “duck interfacing”, gradually becoming documented on demand (but not formally described and verified using a DSL) and I have come to recognize this as a fine solution to a difficult trade-off.

(And this topic is turning into a somewhat off-topic discussion. But as the original question was very hazy and the OP did not show up again, I think this is fine too).

2 Likes

#25

Should we move this to another thread? I’ll let someone else decide.

I suspect that if there were a way to document interfaces in the Julia language then we’d see more documented interfaces. The evidence I have for that assertion is very roughly provided by Python and Javascript/Typescript, where we see a subset (certainly not yet the majority!) of those communities opting in to providing explicit annotations.

I would prefer to have this in the language, so that tooling to provide more checking would naturally arise, and perhaps even some social pressure to write explicit interfaces would come about too if there were a language provided approach.

0 Likes

#26

Some interfaces are already documented, there is nothing preventing anyone from following this practice.

I suspect that the real reason for the absence of many more examples is that good interfaces are rather difficult to design, and evolve organically. At some point people realize that what they implemented can be abstracted as an interface; the threshold is rather fuzzy.

2 Likes

#27

I was unclear. When I said “document interfaces in the Julia language”, I meant having some actual annotation, like the aforementioned interfaces, in the Julia language itself, as was mentioned in the Julia issue I linked to. Any language of course allows external documentation, but that’s as helpful as comments. A language feature would facilitate external tooling, and at least according to the issue mentioned, would not hinder your preferred method of external documentation.

I think it’s worth considering that designers of other dynamically typed languages find the use of types to be useful in very large code bases.

0 Likes

#28

It is not clear to me what the tooling would be in this case.

0 Likes

#29

A static type checker like mypy/pyright/pyre would be great. But I know that “type checking” is actually listed in Compiler work priorities so I suppose the core team is thinking about this as well.

0 Likes

#30

Sorry, I don’t understand how this came up in this context. AFAICT that article is talking about declaring types for variables, eg

In statically typed languages, developers typically specify the type of a variable or a function parameter when they’re declared, for example, using the keyword int to specify an integer, or str to specify a string of characters, to use two simple examples.

Julia already has this: when you specify types for a method, they are effectively checked, and for all other values you have type assertions.

I am not super-familiar with Python and Typescript, but I would suspect that Julia’s problems are somewhat different. With its rich parametric type system, the main problem is not verifying/asserting the type of something (that is trivial), but figuring out what that type should be.

This is a hard problem, and it is not even clear that exposing/specifying this information should be part of an API. Eg if I do

julia> StaticArrays.SVector(1,2,3)
3-element SArray{Tuple{3},Int64,1,3} with indices SOneTo(3):
 1
 2
 3

should the user care about all the type parameters of the result, or are they just implementation details the maintainers of StaticArrays can change at any time? I am inclined towards the latter.

0 Likes

#31

the user should not care, but the developer of packages using StaticArrays needs to know the parameters and if they change later on, this is what semantic versioning is for

0 Likes

#32

I disagree — I would propose that even the packages that use a package should not care about the fine details of its concrete types per se, unless they are part of the API, but then it is probably not the right API.

Abstract types are a different matter. But in most cases those are best left as an internal detail, too, and the relevant functionality should be exposed via traits. My 2¢.

0 Likes

#33

Well, in Grassmann.jl I actually need to use the implementation specific parameters of StaticArrays, otherwise I would not be able to write the @computed struct for the MultiVector type. So, in reality, the details do make a difference, and a change in the parameters would require compatibility changes. In this case, there was no way around it.

0 Likes