In general, I feel that the whole current tactic de jour of utilizing static types is not a sufficiently long term solution to language design. I think the better perspective is to ask ourselves what the clearest, most human communicative visual encoding of a given concept and semantics would be, and then to design languages to get as close to that as possible.

technically assembly is the most least restricted of them all, so it should be the most expressive?

@arcfide right, it's definitely a subjective term, with everyone defining it differently

This essentially translates to: "write a better human-centered syntax for a dynamically typed language with the appropriate compilers/implementation."

@KamilaSzewczyk That's the problem with the term expressive. :-)

Aziz Ghuloum used to remark that Scheme was the language of least restriction, and thus enabled the best expressive power.

And in that sense, APL is most certainly less expressive than Scheme.

On the other hand, APL is more expressive than Scheme in the sense of economy, because APL is capable of expressing more solutions to more problems in more domains with fewer fundamental concepts and fewer abstractions than Scheme.

Given the design intent of APL, which is akin to the design intent of Math, the difficulty of statically typing APL in a useful way can be seen by instead asking the question, "What would be a good static type system for math notation that would be used by people writing math papers in their math papers?"

Notice that this is different than using types as the foundational philosophical and semantic base for the construction of a foundation of mathematics, such as HoTT.

@arcfide it's definitely a balancing act. You want to (or at least I want to, no clue about anyone else) have the type system and non-type system be of about equal "weights" with each doing its part, such that each reinforces the other as well as possible

I think it is important to explicitly frame the question in terms of HCI for the users of the programming language in question.

@dzaima But why? That's the prevailing assumption, but it's not clear to me that this is an obvious good, or why it is obviously better than another solution that doesn't involve a type system and an implementation language.

My current feeling is that the landscape is due for a good existential crisis about types, because they have started to become, if they are not already well entrenched as, a "noble good" unto themselves.

The same goes for everything else, such as object-oriented programming, functional programming, and so forth.

@arcfide The type system helps understanding the non-type system stuff (especially making it much easier to reason about code without much context)

you have a miniature fake type system with variable naming conventions for array vs fn vs op

@dzaima But does it absolutely do that, or is that just the side-effect of having an implementation language that is ill-matched to the problem domain? Is a type system plus an implementation/base language inherently easier to reason about? Or, is a type system a technique for compensating for lack of sufficient expressiveness in the base language? Is it truly the best solution for this, if we also admit the possibility of changing the base language?

@dzaima (since marshall is here, that's kind of my goal in singeli with separating ()-args and {}-args)

@dzaima Note that I don't claim that we shouldn't understand or communicate the types of our programs. But that's something very different than saying that having an explicit secondary notation that always lives with our code as a second meta-programming language is inherently better.

I'm a very firm believer in the use of types in APL programming, and I tend to focus on this in my teaching of APL to new users. But that's not the same thing as static typing.

I think in my previous talk on this I was pretty clear about the very specific focus of "type system" that I generally was speaking about.

@arcfide if types aren't static, imo they lose all their value, aka being able to reason about code with less context

Based on my research, I strongly suspect, but cannot prove, that static typing is less fundamentally effective and usable than finding other means of implicitly communicating type and structural information.

@dzaima See my definition of what I mean when I say "static typing." APL is already statically typed with regards to being able to reason about the code with less context.

@arcfide what are those "other means"?

Syntax, space, names, patterns, &c.

I don't actually have a strict problem with static typing in and of itself. It can be a useful technique.

@arcfide you mean in the video? (sorry, haven't watched it lately)

But it is not a "universally" useful technique.

Yeah, the video.

In particular, I'm in favor of static typing where it can be leveraged as a useful tool to increase the reasonability of code and the ability to gain clarity on that code. IME, I have not yet found a static type system that is able to communicate any sufficiently novel information to the user to enhance or increase the clarity of code on a holistic scale when it comes to APL.

@arcfide I'd call those all "static"

In other words, we should judge a static type system on the basis of whether or not it fundamentally increases the clarity of the code to the human reader absent tooling.

@dzaima I restrict calling something a static type system to those things that match the general expectation of the form of a static type system, which requires the injection of explicit notation into the source code.

Names, spacing, patterns, syntax, and the like are implicit communicators, for the most part, and so they are not part of what I consider a "static type system" for the purposes of discussing static type systems.

@arcfide right, in the APL case I don't see any sane type system either. (i'm not arguing a type system would be good for APL, but more in general here)

Now, that doesn't mean that types don't exist for APL programs, or that we cannot write them down or talk about them. See the Remora type system, the work of Lenore Mullin, the Futhark designers, and more.

Lenore Mullin's work is particularly interesting because she uses APL and types to reason about code, but leverages, in some sense, APL as a type system, not necessarily as a programming language.

So, my point is that the existence of APL as a programming language represents a counter point to the general assumption that static typing is a "good thing(tm)".

Static typing is "good" in so far as it enables programmers to compensate for poor programming languages without changing the poor programming language too much.

@arcfide I don't get why you're playing games with the word "static typing" instead of just picking a different one. It's pretty easy to define, as long as you can agree that the idea of a "type" makes sense. A type error is when an operation is called on a type that it isn't defined on, and a static type system is a way to mechanically prove that type errors don't occur when a particular program is run.

Typed functional languages usually require the entire program to pass type checking while C, Java, etc. have some escape mechanisms like pointer casts that aren't checked statically.

@arcfide I'd very much say that any character subarray of code that gives info about types is somewhat a static type system. (this means that even {2+a} in Dyalog contains "type info" that a must be an array, however obscure that may be. But, of course, static-type-system-ness of a language is a scale, not a boolean value, and Dyalog nevertheless scores badly on it (at least compared to e.g. java))

@Marshall I don't think I'm playing games so much as being more precise about the term and how I'm applying it than what people usually do. People conflate what they mean when they talk about static typing, because they take shortcuts in their definition, and this leads to confusion.

People generally say that APL is not statically typed. But by the definition you just gave, APL is known to be statically typed.

And the definition most people give, or the parts of static typing that they focus on generally are things that APL as a notation already posesses.

@arcfide it's maybe 0.001%-statically-typed. A language isn't just either statically typed or not statically typed

@dzaima The vast majority of people don't use a sliding scale when they talk about a language being statically typed.

my def: "static" means you can figure it out by looking just at the source code (no runtime info)

The most common terms that I have seen are "weekly statically typed", "strongly statically typed", and "dynamically typed", with APL falling into the "dynamically typed" camp.

@arcfide I don't understand. What is the proof mechanism?

@arcfide people do that a lot about many things

@arcfide i think dynamic typing can be weak or strong. how so for static?

Hence the reason I try to be precise about what I mean with regards to static typing as a term.

@ngn The usual consensus is that C is "weakly" statically typed, and Haskell is "strongly" statically typed.

@ngn The problem with this is that it reduces the differentiating power of the term to the point of mostly uselessness, because then all programming languages are statically typed.

ok, what does weak vs strong mean for you? my examples are js (123+"abc" works by converting 123 to a string) vs python (123+"abc" is an error)

@Marshall There are a number of APL implementations throughout the decades that have developed or demonstrated the provability of various levels of static typing over APL programs.

While Dyalog does very little in terms of giving you mechanical access to the types of an APL program, that information exists, and has been proven to exist in the research literature.

@arcfide But if the proof mechanism isn't actually used to reject some programs that you might write, then the language isn't statically typed.

What you're saying is that there exist statically-typed subsets of APL.

@arcfide "that information exists" ≠ I can use it in any meaningful way without first writing more research literature

@Marshall Why? A language is defined independent of the implementation and what features the implementation provides.

@dzaima No one in giving their definition of statically typed language that I'm familiar with talks about the necessity of a real implementation existing.

@arcfide Yes, but if the implementation doesn't perform static type checking, then it implements a different language than the statically-typed ones you're talking about it.

Implementation does not equal language.

apl isn't statically typed under any definition..

@arcfide where am I talking anything about an implementation?

APL as a language is sufficiently statically typed to meet the definitions of static typing given above except my definition.

There is no additional research required. The language has sufficient information in it to reject a number of programs that are erroneous at compile time. Most implementations don't do this. Co-dfns does this for some programs.

Additionally, static typing is not just a tool for rejecting programs. It is often touted as a tool for generating better programs. Dyalog does do this to some degree already.

@arcfide for me, static typing is primarily a tool for localizing information about code

This is my whole point about the need for more precision in the definition of static typing.

@arcfide i'm in the middle of writing something of the sort, if i can manage to

It's become a buzz word in which people don't actually have a clear and precise definition of what they mean, and thus is loses its usefulness.

@arcfide You are equivocating about the term "APL". You're using claims about one language that might be called APL and applying them to a different but similar language.

I don't see how I'm doing that.

@dzaima (and the existence of research papers or whatever proving that APL is statically typed is not at all in any way helpful for me actually reading a function)

@dzaima Sure it does.

lol

@arcfide no!

If I take C, and remove all the type checking (there are still type declarations, but they can be any type at all and it doesn't cause an error), then I get a superset of C that's not, and can't be, statically typed. Just because a subset of it is statically typed (that is, when you add type checking) does not mean the larger language is.

@arcfide you're arguing that an APL that does Magic General Automatic Type Checking™ is better than an actually implemented language that doesn't contain Magic™

If a language would always produce an error at runtime, but that error is now caught at compile time because a compiler recognizes the type information at compile time that would generate the error at runtime and rejects the program at compile time, that is using static typing. Just because an implementation now errors at runtime instead of erroring at compile-time, even though the information exists to error at compile time, does not make the language not statically typed.

No.

I'm arguing that people need to be more precise about what they say and mean when they mean that a given language is statically typed or not.

@arcfide Whether an error can or cannot happen at compile-time absolutely matters for whether a language is statically typed

@arcfide What if it sometimes errors at runtime? Static typing proves errors can never occur for a particular program.

@arcfide i tried

I'm also arguing that one of the reasons that APL doesn't currently admit a useful type system for it is because it already richly expresses that type information sufficiently usefully in the core language so as to make the extra-notational elements of a statically typed variant less useful.

@Marshall Yes, and I'm talking about always erroring.

If a Haskell implementation chose to signal all errors at runtime and not at compile time, that wouldn't make the Haskell language suddenly dynamically typed.

@arcfide for some definitions of the term, it definitely would

@dzaima But that's, again, my point.

The reader of a Haskell program that is using this "dynamic" Haskell variant would still see the same amount of type information and the like as they would from the standard implementation.

@arcfide Then you're not using my definition? If you can only prove that the program doesn't always error, that is, that it might not fail, then you haven't proved that it doesn't have type errors.

To the end user, absent tooling (implementation, &c.), the language itself would be equivalently clear.

@arcfide but they'd see more type information than an APL programmer would see when looking at APL code, hence APL is less statically -typed

@Marshall That's not what I said.

I am rejecting programs at compile time that can be proved to always error and are thus static type errors.

@dzaima Except that this isn't necessarily true.

@arcfide Are you trying to meet my definition or not? You can't just insert an "always".

@Marshall APL as a language contains sufficient type information and is sufficiently studied that there exists a number of programs that can be statically rejected as being type errors at compile time, regardless of whether any of the current APL implementations do this.

@dzaima Except that there are many instances of programs in which the type information for the program and the type intent is much clearer in APL than in other programming languages, such as Haskell, and that this type information can be used by the compiler/implementation much more readily than in Haskell. I disagree with your 99.99% case fundamentally.

@arcfide This is still irrelevant. It's not enough to reject programs that fail, you have to accept only programs that don't fail.

@Marshall In that case Haskell is also not statically typed.

@arcfide Fail with type errors. Is it possible for a compiled Haskell program to do that?

@Marshall Yes, for some definition of type. Many of the researchers at IU were doing research with Haskell programs that contained type errors (they were all called type errors by all the members of the groups) that were not caught by Haskell and would trigger runtime errors.

Even if it is, I suspect it's restricted to particular operations or mechanisms like C and Java, and programs or parts of programs that don't use those are really proven free of type errors.

@arcfide If your goal is to implement a function that adds arbitrary-rank arbitrary-depth arrays following the rules of scalar extension, sure, APLs + is better than whatever mess that'd look like in Haskell. But I don't think the number of cases where APLs permissiveness is helpful is very big.

@arcfide Are they using the definition I gave though? "A type error is when an operation is called on a type that it isn't defined on".

In order for you to talk about only allowing "good" programs through, you have to fix yourself to a specific type system, which is a subset of all types. This is just as possible with APL. So you can have an implementation of APL that will guarantee that the compiled programs will not "go wrong" with respect to a specific APL type system, without ever introducing anything else notationally or otherwise to the APL language.

@arcfide I did condition my definition on the fact that we agree on what a "type" is, and I strongly suspect I wouldn't agree with such a definition.

@Marshall And that's why I think it's very important to very clearly define things like "static typing" and "static type systems" because people aren't precise about this, which is why I was very precise about what I was talking about when I spoke at FnConf on this. It's just not sufficient to talk about this stuff absent some concrete elements.

@arcfide I think I was pretty precise. It feels like I wrote two sentences of definition and you systematically went through ignoring or modifying each phrase in turn to see if you could make headway. This is what I mean by "playing games": you're working as hard as you can to see if you can construe "static typing" in a way that lets you claim that it doesn't meaningfully distinguish APL and Haskell instead of trying to make the definition rigorous and then seeing what the consequences are.

@dzaima This gets back to the "why?" of static type systems (which I define as a specific set of notational syntaxes that are injected into the source code to refine, restrict, or define the types of specific sub-trees of the code). In order to produce meaningful types that will actually reject meaningful things in APL, the end result is that you actually gain less overall information.

One of your original assertions was about being able to reason without context about a piece of code. However, if the notational requirements to reason non-contextually about a piece of code ends up significantly obscuring your ability to see context, then you may actually be doing more harm than good.

@Marshall I have defined my meaning of static typing rigorously.

@Marshall My argument regarding your definition was that it was implying too much.

@arcfide with good type system syntax, you'd be able to easily mentally skip over type information if you don't care about it

@arcfide how so? The resulting code has less meanings, but it contains more information about how it's used and what it does

@dzaima IME with APL, the signal-to-noise ratio with types was so bad that it was unusable. If you can see the entire context of your code in 20 lines or so, but the statically annotated version of that grows to something like 100 lines or so, there's a fundamental clarity reduction with the static annotations. I think people disregard the mental costs of "skipping".

@arcfide right, I'm not disagreeing with that, in the case of APL

@dzaima My point isn't that static type systems are bad.

I never actually claimed that.

I actually claimed that I love static type systems.

What I object to is the viewpoint that suggests that static type systems are a good language design direction currently.

We know that static type systems are useful and usable.

We know that they contribute meaningfully to the usability in many programming languages.

@arcfide I don't think anyone's claiming it's the best direction for absolutely all languages, but it still has a lot of use and does much more good than bad in a lot of cases

@dzaima The problem from my point of view is that it is causing people to reject making fundamental language improvements. They are undervaluing core language design and overvaluing how much total value add exists with static typing.

@arcfide there are plenty of dynamically-typed languages being made still. But if someone wants to make a fast language without reading or writing a couple hundred papers, static typing gives a lot of benefits.

@dzaima I want to see more people working to design languages that are more type-communicative in the core language and that rely less on the static type system to do that for you.

@arcfide Then you need to get some convincing info that that's actually possible without Magic™. Otherwise people will continue believing what they believe in.

@Marshall The main distinction, I think, between your two clause definition and my own is that you define "system" as being an implementation in code that is executable, whereas most of the static type systems that I have seen in my work have no implementation in code, and are just pen and paper implementations. They are still universally called static type systems in the literature.

Additionally, I think generally, that most people think a static type system implies some sort of syntactic explicitness in the source code, and most of the time people don't consider systems that reject type errors but that don't have source code annotations of at least some sort, to be type systems.

unrelated: it's interesting business to try to fit APL characters in 5x9

@dzaima I argue that the existence and usability of APL demonstrates this sufficiently well. There's no Magic there.

@arcfide yeah. Most people care about what they can detect or read, not what the compiler can

@arcfide I don't think APL is much more readable or usable than JS or python

@Wezl if you make a psf font i might actually use it

@dzaima On the other hand, I don't think that the two are unrelated. I think there is a connection and overlap between machine "typeability" and human "typeability". I think there's an area of typability that rests mostly with humans, and an area of typeability that rests mostly with machines, but the area that overlaps is very important, I think.

@ngn I'll make a psf font if you tell me how to use it. I tried making a .bdf before and I had tools to change it to a .psf, a .pcf, and a .hex font, but no format I could use

@dzaima We'll probably have to disagree on that one. :-) But I also think readability is one of those ill-defined terms. A big component of readability to me is judging it without tooling, debuggers, dictionaries, API references, or other forms of documentation. The sole exception I might make to that (and I'm not sold on it) might be the black-box test suite of the programs, maybe the unit tests.

random leftover from unposted things: "type entangledness" might be a useful concept to think about - on how many other "things" the type of a given average "thing" in code relies on. APL has a pretty high entangledness, as the type of pretty much all things requires recursively checking the type of all arguments/invocations up until program input, and Haskell scores low as there are clear borders at which you just know the type of everything (e.g. a single line plus function argument types)

@Wezl (assuming linux) ctrl-alt-f1, and setfont /path/to/font.psf. ctrl-alt-f7 to get back to X

@ngn thanks, I was trying to put it in the directories like .local/share/fonts/ where an otf worked

@Wezl also a FONTX2 from a different tool

@dzaima I've only discussed this as a component of other things, but I'm much more tolerant of entangledness up to some level than I am of obscuring macro-clarity or obscuring macro-level effects/emergent behavior/patterns.

@Wezl for psf there's also a collection of "psftools" that can convert to/from plaintext

Anyways, I'm not sure I actually clarified my position for the original topic, but it was fun. Good to see you @Marshall!

oh, maybe it was because I had .psfu

@Wezl no idea what that is. unicode?

@arcfide the formal definition is not a question of how many limitations you have, but of whether distinct programs have distinct behaviour. (Thus, assembly is not very expressive because, although it has almost no static limitations, most programs written in assembly will crash with a page fault or an undefined instruction.) youtube.com/watch?v=43XaZEn2aLc a good overview

@ngn I think I read something about it being a psf with a unicode table builtin?

@arcfide No, my definition works even in the completely abstract sense of a set of valid source strings and a mapping from source strings to behaviors. The difference I see is that you consider two languages with different valid sets to be the same language. Of course if you consider a language equivalent to the same language restricted to programs that have no type errors then the definition is meaningless! But that's not what a language is.

@arcfide I'm curious about why that is - just the whole array thinking vs JS way of thinking, or something more fundamental?

@arcfide you can do all of these things in any language as long as it's written sufficiently well

js + array thinking = jQuery! :)

@dzaima A given JS program is pretty likely to be statically typeable enough for one to be able to infer the argument types of it. But in APL, many things will work somewhat fine on arbitrary rank & depth arguments, making it much harder to infer the intended arguments, and as such builtin behavior and result

@dzaima "dispatching on type takes so little time, there's no point" <- please change my mind if i'm wrong

@ngn to what is that a response to? (if anything, I'm saying APL builtins having so much runtime dispatching by type is bad)

@dzaima just a general comment about (the pointlessness of) static typing in apl

"there's no point" of having dispatching? of not having dispatching? or having a static type system?

@dzaima of having a static type system

i assume you've read my academic paper about it :)

so "vtables/switches are efficient, therefore static typing is unnecessary"? sure, performance-wise, but the nature of APL means you are often forced to either consider all paths, or follow through the mess of dynamic type argument to understand whether your ⍵ is a matrix or a vector

in f←{×⌿⍺∘.+⍵} you almost want to just assume ⍺ and ⍵ are vectors. Which works, I guess, but isn't a very nice way of dealing with the problem that you just don't know

To accurately capture the requirements you need dependent types as well :(

@dzaima f←{assert 1≡≢⍴⍺⋄assert 1≡≢⍴⍵⋄×⌿⍺∘.+⍵} problem solved :)

@ngn and now you've made a pseudo-type-system

no, just a runtime check

@ngn define assert as {⍵:1⋄__builtin_unreachable⍬} :p

@dzaima ok you're right

@ngn now run that with 1 and 'a'

for some definition of right :)

@rak1507 presumably the assert will fail when given a falsey arg

oh that should be (,'a') and (,1)

@rak1507 It's not a proper full type specification, but it is an increase in information locality, which is what a type system achieves

fair enough

with the asserts, you can fully infer that the arguments are supposed to be numeric vectors to not get an error, therefore losing all entanglement with the surrounding context

if apl had macros to disable the asserts for a "release" version, it would be even better

@dzaima (actually you'd also need to specify that the arguments have depth 1)

details..

@ngn yep. The thing that cripples any chance of an APL type system being practical

@dzaima (to be fair, that doesn't change much. you'd need {⍵:1⋄__builtin_require_unreachable⍬} or something)

@dzaima (better known as static_assert)

ermineii.github.io/paste/#0bZLBboMwEER/…

turns out slash-bar is the ugliest with my constraints

argh, unicode put ○ in geometric shapes

<moon-child> iirc ⊤⊥ are in the math section but ⊢⊣ are in the apl section

Ooh, a whole lot of discussion while I was sleeping

yeah a rare aaron hsu appearance