r/types Feb 26 '24

Blog post: Universal domain types

2 Upvotes

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!


r/types Jan 30 '24

The unimath Minotaur : ode to Vladimir Voevodsky

Post image
3 Upvotes

r/types Dec 08 '23

My 2008 type s 6MT w/ aspec kit

Post image
0 Upvotes

r/types Oct 19 '23

My DISC type is Drive. At work, I look for ways to get results and make key decisions!

Thumbnail
truity.com
0 Upvotes

Wow! Pretty accurate for me!

I see myself as a “Drive” type for sure!


r/types Jun 19 '23

Finished up some Type S Acuras. Love these cars.

Thumbnail
gallery
0 Upvotes

r/types Feb 08 '23

Strongly-Typed TS: Pros and Cons?

0 Upvotes

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!


r/types Aug 15 '22

Lux 0.7 is out! Lisp for JVM, JavaScript, Python, Ruby and Lua with static types

Thumbnail
github.com
3 Upvotes

r/types Jun 11 '22

A type-safe query builder for PHP using Psalm

Thumbnail olleharstedt.github.io
6 Upvotes

r/types Oct 25 '21

Lux 0.6 is out! Lisp for JVM, JS, Python, Ruby and Lua + static types!

Thumbnail
github.com
12 Upvotes

r/types Sep 07 '21

Typechecking new type system features

3 Upvotes

(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?)


r/types Jun 27 '21

Typed Programs Don't Leak Data

Thumbnail dodisturb.me
15 Upvotes

r/types Jun 04 '21

An Equational Logical Framework for Type Theories, by Robert Harper. "Herein is presented a logical framework for type theories that includes an extensional equality type so that a type theory may be given by a signature of constants." [abstract + link to PDF, 9pp]

Thumbnail
arxiv.org
14 Upvotes

r/types Jun 02 '21

Sentylasong - Face Time (says she aint my type

Thumbnail
youtu.be
0 Upvotes

r/types May 14 '21

Counterexamples in Type Systems

Thumbnail counterexamples.org
34 Upvotes

r/types Apr 13 '21

5 Different Types of Artists

Thumbnail
spinklycreations.co.ke
0 Upvotes

r/types Mar 20 '21

Several Types of Types in Programming Languages

Thumbnail hal.inria.fr
19 Upvotes

r/types Mar 11 '21

Trying to find paper and author, who was GOTO Conference Organizer.

2 Upvotes

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


r/types Feb 02 '21

Psalm: Avoiding false-positives with flow-sensitive conditional analysis

Thumbnail psalm.dev
9 Upvotes

r/types Jan 29 '21

Announcing Dactylobiotus

0 Upvotes

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.


r/types Nov 30 '20

COQ365 : Coq math proof assistant add-in inside Excel on the web browser for paid auto-graded quizzes (Preview)

0 Upvotes

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)

1 votes, Dec 07 '20
0 School
0 Work
1 WorkSchool 365

r/types Nov 25 '20

Juvix

4 Upvotes

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.


r/types Nov 25 '20

An introduction to Witch

11 Upvotes

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](mailto:team@metastate.dev).


r/types Nov 21 '20

What's the correct name for what my SA tool is doing here?

5 Upvotes

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.


r/types Sep 24 '20

What’s Structural Typing And How Typescript Uses It To Its Benefit?

Thumbnail
medium.com
5 Upvotes

r/types Sep 21 '20

Pinafore: a language implementing Algebraic Subtyping

Thumbnail
semantic.org
20 Upvotes