I love types! As with most things in life, we can get 80% of type safety benefits with only 20% of extra effort. I wrote a blog post about simple classes of domain types that appear in almost any program but which most programming languages fail to make convenient to define: Universal domain types.

I’d love to hear your feedback. And if you know more examples of such type classes, please let me know!

Hello everyone!

I've recently been exploring the world of TypeScript and have been hearing differing opinions on the use of strongly-typed variables versus inferred types. Some videos I've watched claim that inferred types are more trustworthy, and others say that you can lie with deferred types.

For example:

https://www.youtube.com/watch?v=I6V2FkW1ozQ
https://www.youtube.com/watch?v=kRiD6ZpAN_o
https://www.youtube.com/watch?v=RmGHnYUqQ4k

What are your thoughts on this topic? Do you have any experience using strongly-typed variables in TypeScript, and if so, what have been your biggest challenges and benefits?

Looking forward to hearing your thoughts and experiences. Thank you!

(Just a note, this is not only a question about making sure it's possible, it also about how to actually implement these things in the typer)

Hello, I'm the developer of the Star programming language, and I have some questions about how to typecheck several new/uncommon features that it has, and looking for feedback on it in general.

For reference, Star is a highly experimental language that's focused on powerful features and consistency, which is also reflected throughout the type system. It has many features that are either very rare to find (e.g. type refinement/overloading, safe multiple inheritance), or are completely brand-new ideas that don't exist anywhere else (from what I've been able to find online). Because of that, it's been hard to find good resources on how I should go about typechecking this stuff (or even how to structure some of it), and anything that I do find is usually covered with too many Greek symbols for my liking.

Here's a list of the things I've had the biggest issues with, with a brief description for each thing (more docs can be found here):

Extensible/class-like variants

Should be self-explanatory, but I'll go a bit further anyways.

For the longest time, variants have been very limited and therefore relatively easy to typecheck (excluding GADTs). In Star, variants are given a lot more features such as being able to inherit classes/other variants, implement protocols, and define methods and instance fields (all of this in addition to the fact that type refinement gives you gadts for free).

The obvious issue here is that you can't sanely verify that pattern matching is exhaustive like this, and multiple inheritance also makes it a bit funky. There's also this other neat feature where variants can act similar to bitflags, even variants that store values. Not even sure if things like instance fields and gadts could work with those, which is also a bit problematic.

As far as I know, there are only 3 languages that do anything close to any of this:

• OCaml supports polymorphic variants, but they don't have a real inheirtance chain nor do they support instance fields.
• Nemerle supports instance fields, methods, and inheriting from classes / implementing protocols, but not inheriting from other variants.
• Hack supports multiple inheritance for Java-like enums and nothing else, which is otherwise pretty useless here.

So yeah, not sure how to verify exhaustivity (if it's even possible), implement GADTs, or what to do about the bitflags thing.

Also, having polymorphic "this" types (as seen in TypeScript and Scala) kinda blows the variant subtyping thing out of the water, rendering OCaml's strategies useless as a bonus.

Typeclasses

I'm not sure how to best explain this, but it seems to me like I need some unholy mix of C++, Nim, and Scala 3 (it's honestly easier to just read the docs lol).

Typeclasses are exactly what you think they are, but also a bit more just for fun. Typeclasses are really just (unbound) type variables that are captured by a type alias:

type T { on [Str] }
alias Stringy = T

This apparently causes some issues, especially when you have multiple unbound typevars:

type T
type U of Foo[T], Bar[T]
alias Thing = U

For maximum enjoyment, assign Thing to T instead. Theoretically you can typecheck it, but I have no clue how to even go about doing that.

Now mix in type conditions (type T if T != Foo && Bar[T] <= T), and I'm now completely lost. As far as I know, Nim is the only language with typeclasses this powerful, and even then they're extremely unstable.

Oh yeah there's also multi-param typeclasses and multiple instances per typeclass are allowed, unsure how many more issues that causes.

Categories

Please just read the docs and you'll figure it out pretty quickly lol.

Misc

• Partial initialization: Exactly what you'd expect, except that it also has to work with subtyping and all the other fancy type stuff. How? dunno lol
• Capturing outer type variables, which is an unintentional feature that should probably work anyways (to some extent?)

Uh anyways, I hope that explained things enough. I was recommended by a friend to ask about these things here, so any help/feedback is appreciated.

(btw is it better to ask stuff on zulip, the mailing list, or here?)

Trying to find end of 1990's paper and name of author mentioned @39:48, Kristen Captoro (?) goto conference organizer.

https://youtu.be/0lXUBVipXa8?t=2380

We are pleased to announce Dactylobiotus, the first developer preview release of Juvix. The aim of Juvix is to help write safer smart contracts. To this end it is built upon a broad range of ground-breaking academic research in programming language design and type theory and implements many desirable features for a smart contract programming language. This first release supports compilation to Michelson. As the Juvix language is written in a backend-agnostic fashion, future releases will support additional backends. To learn more please visit the following links: blogpost, official website, Github

Let us know if you try it and have any feedback or suggestions.

Business aspects of programming languages toolchains ? (elearning + ecommerce)

This question is more valid when the programming language in question is a proof assistant, that is it can be used to introduce mathematics & logic to learners at school.

The first keyword in the last phrase is : "introduce". Therefore asking learners to buy a 32go RAM computer, install linux and emacs, just to see what this fancy new "assistant" is about, would not be considered very "introductory". Things need to happen in the web browser.

The second keyword is : "school". Therefore there needs some to be some way to engage, quiz and test learners and to certify transcripts. The best way to engage people is : money. When money is involved, people are motivated. So there should be a direct way to traffic knowledge in exchange for money payments, in addition to the indirect way via government funding.

So what is the solution, you asked?

TL;DR: WorkSchool 365 is a paid auto-graded quiz that embeds the Coq proof assistant add-in inside Excel on the web browser!

Sign-in as a learner worker to traffic your quizzes and other academic events for real money payments (with PayPal + China's Alipay...)

Sample Coq quizzes ( Table of Contents (Initial) , 4. Classification ) :

"Q1. The keytext « fix F (n : nat) : P n := ... » above says that

• (A) the precise-classification « P n » of the output value is fixed and does not depend on « n ».
• (B) the value of the output is fixed and does not depend on « n » .
• (C) the identifier « F » may be mentioned in the definition ( right hand side of « := » ) of itself."

P.S. this is part of larger collaborative attempts by those WorkSchool 365 learners workers to implement the new proof assistant MODOS of homotopical computational logic for geometry; MODOS is motivated by cut-elimination in fibred-categories (Dosen, Petric...) and by local projective universal-homotopy categories of sheaves (Cartier...) Reddit, tell us what is your prognosis on this new crazy theory?

P.P.S. We are hiring! - WorkSchool 365 Learner Worker Q&A - Job Interviews & Enrollments @Friday 4th Dec 18:49 PM (UTC+1)

View Poll

Juvix synthesizes a high-level frontend syntax, dependent-linearly-typed core language, whole-program optimisation system, and backend-swappable execution model into a single unified stack for writing formally verifiable, efficiently executable smart contracts which can be deployed to a variety of distributed ledgers.

Learn more about Juvix by watching Christopher’s presentation hosted by Nomadic Labs. Visit Juvix’s website, and follow Juvix’s twitter profile to learn more.

We published an introduction to Witch here. Witch combines different proof strategies to enable users to profit from proof assistants without an in-depth understanding of the theory behind it.

To learn more about Witch, please follow this link. To learn more about Juvix, visit this website. For feedback or questions, please do not hesitate to contact us: team@metastate.dev.

I created a static analysis tool for PHP named Psalm, and a few years ago I gave it the ability to do a bit of very simple SAT solving.

Is there an official name for what it's doing here to infer the type of $b? Are there other analysers that do this too?

https://psalm.dev/r/783b6e9ee1

No other tool in its category of dynamic language typecheckers (TypeScript, Flow, Hack etc) performs this particular inference, and I was wondering whether it's interesting-enough to write up. The feature has proven very useful when analysing convoluted PHP code.

A dynamically typed numeric tower? easy. Statically typed? HELP. I'm making a static type checker for my functional language extending https://www.cl.cam.ac.uk/~nk480/bidir.pdf (im calling it DK13 for simplicity)

At first I've tried hardcoding int <: float <: complex <: number and then adding synthesis rules for basic binary arithmetic operators (addition and multiplication). I have spent many days piling up sketches on sketches of inference rules to extend the DK13 type system, with no luck. Synthesis breaks when abstracting a binary operation referencing an existential. This is what I'd like to achieve (=> is for synthesizes)

(λ x -> (x+1))(2.4) => float
(λ x -> (x+1))(2) => int
(λ x -> (x+1))(2+3i) => complex
(λ x -> (x+1.3))(2.4) => float
(λ x -> (x+1))(2) => float
(λ x -> (x+1))(2+3i) => complex
and so on... you know dynamically typed numeric towers

I added similar (perfectly working) rules for if-then-else statements: they synthesize to the supertype between the types of the two branches. One of the two branches MUST be a subtype of the another, or the if-then-else expression fails to synthesize. This was easy.

A similar approach for simple arithmetic operations breaks because any existential variable referenced by the expression gets solved to "number" if add a premise stating that the operands must be subtypes of number. If i delete the check that both operands subtype number, it works perfectly but allows nonsensical expressions like "hello"+5 to horribly be allowed by the typechecker.

I then started reading https://www2.ccs.neu.edu/racket/pubs/padl12-stff.pdf

Suppose I have a substitution function of type (var -> term) -> term -> term, that is, it recursively replaces free variables for terms in the usual way. If the first argument function is injective, is the resulting function injective?

Edit: This is not the case.

For more context, I stumbled upon this question while formalizing untyped lambda calculus in Lean. Most functions dealing with renaming are injective, so I thought maybe substitution also was.

My formalization is work in progress, most injectivity lemmas can be found here while the complete substitution implementation can be found here. Note that subst_ext σ is injective given σ is (as I wrote in a comment, this does not hold for subst σ).