[h0l0cube]

> This is not something I've read about casually on the internet

Was speaking specifically about your opinions on Dialyzer and Elixir. It's very much a cursory Google around and having stronger opinions about the limits of a language than people who spend time with the language.

> You've graduated from saying "I think someone more savvy with Elixir would know more."

It took further reflection on the idea. It helps to start with at least some epistemic humility, once again the crux of this thread. I'm willing to revert to, "It ought to be possible" given that macros boil down to the final generated code (including typespecs) which is then analyzed by Dialyzer

> Elixir is just as good at dependent typing as Idris, which has that feature built in?

Metaprogramming allows features to become 'built in'. e.g., being able to integrate type checking and compiler errors for HTML/XML or other DSLs.

https://hexdocs.pm/eex/EEx.html#function_from_string/5 https://hexdocs.pm/phoenix_live_view/0.17.0/Phoenix.LiveView...

[Vaguely2178]

> Was speaking specifically about your opinions on Dialyzer and Elixir. It's very much a cursory Google around and having stronger opinions about the limits of a language than people who spend time with the language.

I think your experience with Elixir and Dialyzer (or perhaps emotional attachment to these tools) is blinding you to the fact that there are features that your favorite language lacks. I gave you a concrete example of something that's a research topic in Elixir (inferring types from guards), which has an existent analogue in TS (type narrowing). You completely ignored that and fixated on the one sentence about experience. Your entire argument is that I should defer to your authority on the topic as an anonymous commenter, because you're supposedly very experienced. It feels like a very hollow appeal to authority.

> It took further reflection on the idea.

But by your standards simple reflection is not enough to establish authority on a topic. You need to have deep personal experience with using macros to parse text before you're qualified to make a firm judgement. You event went so far as to speculate on how TypeScript implements type checking and claimed that the "secret sauce" is probably metaprogramming, despite having never worked on the compiler. This all feels incredibly contradictory.

> Metaprogramming allows features to become 'built in'. e.g., being able to integrate type checking and compiler errors for HTML/XML or other DSLs.

Built in does not mean "I might hypothetically be able to write my own macro that does this". It means it already exists in the language today.

Honestly this discussion feels like it's devolved into repetitive bickering, which is why I let your original comment about metaprogramming stand unanswered, and you reacted by following me into a different comment thread to reiterate the point.

[h0l0cube]

> emotional attachment to these tools

You've really misjudged me. I've been programming professionally for 20 years, I have used and still use a variety of languages including Typescript.

> Your entire argument is that I should defer to your authority

Never made such an argument. My argument is that you have less authority on the subject matter than someone who has spent years with the language.

> I gave you a concrete example of something that's a research topic in Elixir (inferring types from guards), which has an existent analogue in TS (type narrowing)

At best a subset of functionality than an analogue. This kind of research is being conducted by experts in type theory outside of Elixir. If it's a problem for Elixir, it's a problem for any other language that would attempt it, and absolutely I would defer to the authority of those experts who have spent years looking at type theory.

> despite having never worked on the compiler

Knowledge of meta-programming doesn't require the same skillset as writing a compiler. I'm certain you or any other capable software engineer, would be able to write a macro that parsed JSON, interrogated the typing of that JSON, and spat out a typespec with some knowledge of Elixir `defmacro`, `quote`, and `unquote`.

> Built in does not mean "I might hypothetically be able to write my own macro that does this".

Never made such a claim. My claim is that the JSON typing mechanism isn't really something that's dependent on the Typescript language and toolchain. As with my link on my last post of inline heex components, it's possible to take a text representation of something in Elixir and transform it into something that's available to the compiler (and hence also available to Dialyzer).

> bickering

Trust me there is no spite from my end.

[Vaguely2178]

> At best a subset of functionality than an analogue. This kind of research is being conducted by experts in type theory outside of Elixir. If it's a problem for Elixir, it's a problem for any other language that would attempt it, and absolutely I would defer to the authority of those experts who have spent years looking at type theory.

Ironically the researcher that you're deferring to (Giuseppe Castagna) wrote a paper about the set theoretic types Elixir is hoping to implement one day, and he points to TypeScript as a practical existent example of these types. This is the same paper Elixir's creator recommends as an introduction to the research [1]. The paper is called "Programming with union, intersection, and negation types" [2]. Here's a quote from the conclusion of the paper (page 55):

"...the need of set-theoretic types naturally arises when trying to fit type-systems on dynamic languages: union and negations become necessary to capture the nature of branching and of pattern matching, intersections are often the only way to describe the polymorphic use of some functions whose definition lacks the uniformity required by parametric polymorphism. The development of languages such as Flow, TypeScript, and Typed Racket is the latest witness of this fact."

You might also want to take a look at the discussion that took place on HN about the paper when it was published [3].

[1] https://elixir-lang.org/blog/2022/10/05/my-future-with-elixi....

[2] https://arxiv.org/pdf/2111.03354.pdf

[3] https://news.ycombinator.com/item?id=32018751

[h0l0cube]

> wrote a paper about the set theoretic types Elixir is hoping to implement one day

The point is, if a solution already exists, it's implementation details would simply be imitated and no further research would be required. The SOTA in set-theoretic types is not sufficient to capture typing for guards, which last I heard was a focus of Castagna's research specifically for Elixir, though the sophisticated typing of Elixir may also present other significant challenges.

Again, type narrowing isn't related to pattern matching on guards. As far as I'm aware, pattern matching on function signatures is impossible for Javascript as it doesn't even permit function overloading - though Typescript could do name-mangling like C++ does to get around this. Guards allow you to overload functions based on the shape of the data, and guards can be quite complex when chained together (e.g., 'and', 'or').

But to refer back to the stated project goals, its aims are more ambitious than the SOTA:

> - The Elixir team wants to go beyond type annotations and make type signatures a direct part of the language in a way to add new idioms and expressive power to the engineering teams that opt-in. This should open new perspectives in the theory of typing and the application of bi-directional typing.

> - The language and runtime of Elixir have a distinct focus on fault-tolerance, concurrency, and distribution, which can lead to interesting typing considerations and modelling

https://www.irif.fr/~gc/stageElixir.en.html

[Vaguely2178]

> The point is, if a solution already exists, it's implementation details would simply be imitated and no further research would be required.

Imitating ideas from one language to improve another is a form of research, and can be fairly difficult.

> As far as I'm aware, pattern matching on function signatures is impossible for Javascript as it doesn't even permit function overloading

There's no syntactical support for function overloading in JS, but it's fairly trivial to accomplish the same semantics using normal control flow (i.e. conditionals). This is why type narrowing (which uses control flow analysis), is relevant here. The paper I referred to above actually points this out. On page 6 under the section labeled "FUNCTION OVERLOADING", the author wrote:

"However, intersection types let us express ad-hoc polymorphism (i.e., function overloading) if coupled with some mechanism that allows functions to test the type of their arguments."

The author then goes on to describe this technique in more detail on the very next page:

"OCCURRENCE TYPING: Occurrence typing or flow typing [59, 46, 17] is a typing technique pioneered by Typed Racket that uses the information provided by a type test to specialize the type of some variables in the branches of a conditional...This method of refining types according to conditionals is important in type systems for dynamic languages and in those that enforce null safety: some examples include Ceylon [38], Dart [27], Flow, Kotlin [37], Typed Racket, TypeScript, and Whiley [47]."

> But to refer back to the stated project goals:

Thank you for linking to the list of project goals. The second bullet point under the list of goals says:

"To capture some programming patterns used in Elixir programming one needs to resort to the techniques of gradual typing, parametric polymorphism, and occurrence typing, three tools whose theoretical aspects have been already studied for semantic subtyping".

TS of course exhibits gradual typing and parametric polymorphism (generics), but did you notice the mention of occurrence typing? The same form of typing I referred to above, and which the author explicitly mentions exists in TypeScript (amongst others).

I honestly don't have the time to devote to this conversation any longer. I will most likely allow you to have the final word, because this discussion could carry on ad infinitum and is incredibly unproductive. As Paul Graham once said this might be taken as a tacit admission of failure [1], but I have things to do.

[1] https://news.ycombinator.com/item?id=34043420#:~:text=when%2....