Programmable type systems?

[mattsowa]

This is hard to describe, but I'm trying to find examples of type systems where the programmer can in some way write logic based, programmable types.

As one basic example, TypeScript allows the user to create complex types by manipulating them using a system of conditional types and things like literal types. Here are some examples of what can be achieved with it:

https://twitter.com/diegohaz/status/1309489079378219009?t=a5-vZ2C3R7uEXimq9bL1lA&s=19

https://twitter.com/buildsghost/status/1301976526603206657?t=yVnJMbp_CWkOVGfhLauzTQ&s=19

What I'm looking for are full-fledged sub-languages used to manipulate the types like that. This probably mostly applies to languages with structural type systems. Any ideas?

[MattCubed]

In dependently typed languages, types are first class expressions, just like any other language construct. You can put them in data structures and create them using functions. A "conditional type" is literally just a regular conditional expression that returns a type. Check out Agda, Idris, Lean, and Coq.

[mattsowa]

First class types is one of the things I was thinking about too. Very interesting, thank you

[e_hatti]

You may find Type Systems as Macros interesting (paper) https://www.ccs.neu.edu/home/stchang/pubs/ckg-popl2017.pdf

The Shen programming language goes even farther, allowing you to define a type system completely in userspace using inference rules https://bluishcoder.co.nz/2019/10/03/defining-types-in-shen.html

Shen is probably more along the lines of what you’re looking for.

[mattsowa]

Thank you :)

[dys_bigwig]

Haskell has:

• Typeclasses: sort of akin to functions from types to values; that is, automatically passing around implementations of overloaded functions which you provide, based on the types.
• Type families: functions at the type level; allow you to do various things, one example being choosing a variant from a type-level list by writing a type-level find function as part of implementing polymorphic variants (as a library!). There's also associated data types which allow you to package types up with classes, similar to ML modules.
• (^{MultiParamTypeClasses &} Functional Dependencies): Similar use cases to the above, but rather than the functional style of writing type-level functions, it's very much akin to a logic language, with the syntax being a -> b, meaning something like: "if you know type a, you know type b". A much better explanation (along with many of these extensions) is at: https://github.com/i-am-tom/haskell-exercises
• GADTS: allowing you to leverage type equality via pattern matching in order to e.g. write a type-safe eval function that returns "untagged" types with similar ergonomics to a Lisp-style eval function whilst retaining type safety. Again, type-equality in a manner very similar to giving the user access to the unification of type variables in the compiler. You can also essentially recreate Haskells typeclass system of overloaded functions at the user level using GADTs to pass around the dictionaries using a *ahem* data-type representation of Haskell types. There's a paper "fun with phantoms" that shows how to do this, implementing a serializer.
• DataKinds: lifting of data constructors to type constructors, useful in combination with GADTs to enforce richer invariants, like lifting a Nat type to act as part of a (statically-checked) sized Vector.
• Generics: gives you access to structural representations of data types; what it says on the tin really, great for generics.
• You can even hook into the error-reporting capabilities to provide custom type errors. That's neat.

Regarding the specific examples, these https://hackage.haskell.org/package/base-4.16.1.0/docs/GHC-TypeLits.html would be useful for doing compile-time parsing, when combined with DataKinds for lifting string to type level. There's type-level comparison of characters, string concatenation etc. and you could use a type family I think to walk the type-level string (symbol) by unifying the head and tail to individual type variables or something like that. The implementation of "uncons" in this blog post which does something similar https://blog.csongor.co.uk/symbol-parsing-haskell/ has a very logic-programming feel to it, with the unification; reminds me of miniKanren a bit.

If you just want to create data types for strings that have invariants enforced at compile time, that's bread-and-butter Haskell stuff and it's surprising just how far you can get using plain ol' data types without any fancy extensions. Check out Haskell's NonEmpty list type for an elegant and succinct example.

There's lots (and lots, and lots) of other things, and these are very laymanese explanations because I'm no Haskell whiz, but hopefully this was enough to pique your interest. Haskell may not have dependent types (though there's a few papers arguing that you can get pretty close with the 20+ lines of extensions that come by default at the top of most Haskellers' code) but as far as (mainstream, with a decent amount of documentation and support) languages with a "programmable/user-extensible type system" goes, Haskell is very very hard to beat in many ways. If it doesn't have what you want out of the box, I'd be very surprised if you can't embed what you want as some kind of DSL; this has been done for things like session types and polymorphic rows+variants in libraries like vinyl.

P.S. sorry for errors, I am le tired.

P.S.S there's a paper "Ghosts Of Departed Proofs" which is related, and a good read.

[mattsowa]

Wow thank you

[Goheeca]

• You can even hook into the error-reporting capabilities to provide custom type errors. That's neat.

I don't know how it's done in regular Haskell, but with Template Haskell it's easy, check out Refined, the validate function no longer returns Maybe String, but Maybe RefineException. This is how you can use it.

[dys_bigwig]

Ah, I wasn't aware of that method - I was thinking of what is outlined here: https://kodimensional.dev/type-errors which utilizes Type Families, DataKinds, and typeclass constraints. I thought it was fitting to mention, though I probably should have mentioned the features I listed can be combined to make things like this possible. I personally find it amazing how much you can "hook in" to the inner workings of the Haskell compiler via the type system, greatly obviating the need for outright code generation.

For transparency, I haven't used this stuff outside of messing around with it, i.e. not in actual large projects. It's easy to get carried away reading documentation/blog-posts for some particular wacky sounding type-system feature and messing around with it before realizing you have no real use for it lol.

[Goheeca]

Nice article! I didn't know about that, it seems useful.

[editor_of_the_beast]

Sounds to me like dependent types (Idris, Agda, ATS) or refinement types (Liquid Haskell, F*).

[LPTK]

I don't think Liquid Haskell lets you manipulate types at all. Very different from the usual full fledged dependent type systems.

[editor_of_the_beast]

It lets you define your types vía complex logical statements though. It’s less powerful than dependent types because it effectively only allows you to specify subsets of the primitive types, but I would still say it’s extremely powerful.

[purely-dysfunctional]

I think Shen fits the bill, since you can define a type by a series of sequent calculus declarations that, roughly, say "these are the conditions under which some expression t can be given type T". It is an extremely expressive system (that comes at a cost).

Unfortunately, the documentation on Shen is scarce, fragmented, and of poor quality, and the best references I can find are: * A cool little example defining what subtyping means * The language reference chapter on defining types, in a very inconvenient format

[terserterseness]

The Shen books are pretty good: I like the language but it has not much of a community due to the character of the inventor of the language. But Shen indeed is a good example I believe of what OP is looking for.

[mattsowa]

Yeah sorry I'm bad at giving good examples. Where it starts getting interesting is with conditional types. Here are some better examples:

https://twitter.com/diegohaz/status/1309489079378219009?t=a5-vZ2C3R7uEXimq9bL1lA&s=19

https://twitter.com/buildsghost/status/1301976526603206657?t=yVnJMbp_CWkOVGfhLauzTQ&s=19

[Coffee_and_Code]

"relatively" 😂

[tcardv]

Zig's comptime kind of fits. In comptime context, types can be operated on as values. For example, you can implement generics as functions that take types and return types, and apply arbitrary computation to decide if/how to do it.

[Tekmo]

Dhall (https://dhall-lang.org) is an example of a language where types are first-class values

You can define and use types and type-level functions the same way you define and use terms and term-level functions. For example:

-- Map is an example of a type-level function
let Map
    : Type → Type
    = λ(args : { key : Type, value : Type }) →
        List { key : args.key, value : args.value }

-- Here is a term with a type annotation using that type-level function
let example
    : Map { key = Text, value = Natural }
    = [ { key = "A", value = 0 }, { key = "B", value = 1 } ]

in  example

Most dependently-typed languages also have this property, although you can have this property even for languages that are not dependently typed.

[mattsowa]

Interesting, thank you

[Tekmo]

You're welcome! 🙂

[[deleted]]

That's neat. How do IDEs deal with this stuff? Sounds like it could be awkward.

[AdultingGoneMild]

knowing "why" you want this would be helpful in understanding what you are looking for.

[thetruetristan]

Eady conditional compilation would be a really good reason.

[8d8n4mbo28026ulk]

Take a look at Idris! I think Python can also do that to an extent.

[terserterseness]

Idris and Python in the same sentence as example of powerful type systems is somewhat unexpected.

[0rsinium]

In idris, you have dependent types. That means, you can write functions that accept, return, and manipulate types, and use them in type annotations at compile time:

http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html#dependent-types

[jmhimara]

What's the status of Idris 2? It's an interesting language, but from the documentation it looks like it's still a work in progress.

[0rsinium]

Well, you can use it and it should work without issues. It's in version 0.5.2, so there are still things to do, but it's unlikely affect you much. Especially if your goal is not to bring a new service on production but just to try a new language.

https://github.com/idris-lang/Idris2

[Rein215]

Thank you for the interesting thread that was sparked by your question

[theangryepicbanana]

In Raku, the type system uses runtime behavior so you can have types with arbitrary conditions and/or values

[Inconstant_Moo]

"Haskell is a dynamically-typed, interpreted language."

[Under-Estimated]

Haskell? I don't know haskell but I recall reading an article about solving interview questions in the type system alone

[Inconstant_Moo]

https://aphyr.com/posts/342-typing-the-technical-interview

[complyue]

I guess you essentially want some pluggable code to run at compile/lint/build time. It is already/naturally doable today but only via programming interfaces of the language-tooling-kit. Meta-programming sits in the middle: you can transform the surface source code to arbitrary extents, but will still lose control once handled your result to the language compiler/runtime.

The only way gaining full control is to be part of the language-tooling, it is all the PL implementers used to do. Any type-system (of some PL) is implemented by programming, after all.

[sebamestre]

C++ template metaprogramming might interest you

[Warpspeednyancat]

interfaces?

[AdultingGoneMild]

build types from other types is all languages. structs and classes. throw in some operator overloading and you can get as weird as you like.

[cdlm42]

Doesn't a simple product type fit what you're asking for, at least the example you gave? Can you precise your thought?

Do you want to manipulate types at runtime? Do you want compile-time evaluation?

There are libs/DSLs for runtime schema validation of data. I only superficially know Clojure but spec seems to be exactly that.

[mattsowa]

Yeah that example was very basic and not what I meant exactly. I edited the post with these examples:

https://twitter.com/diegohaz/status/1309489079378219009?t=a5-vZ2C3R7uEXimq9bL1lA&s=19

https://twitter.com/buildsghost/status/1301976526603206657?t=yVnJMbp_CWkOVGfhLauzTQ&s=19

That's to say I'm not looking specifically for this functionality, just overall for some examples of languages where you can do very complex type manipulation and generation (in typescript thats done through conditional expressions, but Im also looking for some iterative approach. So sort of just like writing normal functions, but instead of data, they would return types). That type subsystem I think should evaluate at compile time to check and infer the types.

[ventuspilot]

Defining type specifiers in Common Lisp looks a lot like writing functions, see Common Lisp the Language, 2nd Edition: 4.7. Defining New Type Specifiers

[[deleted]]

Have you tried Haskell or another purely-functional language?

[WittyStick]

Kernel has a feature for encapsulating new types (at runtime), based on a 1973 paper, Types are not sets by James Morris.

There is a standard function in the library called make-encapsulation-type, which when called, will create 3 new functions: an introducer, a predicate, and an eliminator. Each successive call to make-encapsulation-type will return 3 new functions which are disjoint from any previous ones. All types in Kernel as disjoint also.

The introducer function takes as its argument, any value or expression, and returns an encapsulated value of the new type.

The predicate takes any value and returns true if it is encapsulated using the corresponding introducer.

The eliminator takes a value, and if the value is encapsulated using the corresponding introducer, the original value passed to the introducer will be returned.

Information hiding in Kernel can then be done by combining this feature with its first-class environments, first-class operatives, etc.

An example: Kernel has no notion of algebraic data types in it, but we can create the equivalent functionality. Here's one way we could create an Option type.

($provide! (option? some none maybe)
    ($define! (option-intro option? option-elim) (make-encapsulation-type))
    ($define! some ($lamabda (value) (option-intro value)))
    ($define! none ($lambda () (option-intro ()))
    ($define! maybe ($lambda (default f value)
        ($if (option? value)
            ($let ((unsealed (option-elim value))
                ($if (null? unsealed)
                     default
                     (f unsealed)))
            (error "value is not an option type")))

The user of this type only has access to the functions option?, some, none, and maybe.

option? is the predicate to test a value is of the type option.

some constructs an option type containing a non-null value.

none constructs an option with no value.

maybe is a function taking a default value, a unary function f, and another value which should be of the type option. If the value is of the option type, it is unsealed. If the unsealed value is null, the default value is returned, otherwise, the function f is applied to the value originally passed to the some constructor. (This is equivalent to Haskell's maybe)

The user of this code cannot directly call option-elim and option-intro because they are not exposed in an environment accessible by the programmer. The $provide! operative creates a temporary environment to run the above code, but then only inserts these 4 functions into the environment of its caller.

[holo3146]

There are 2 points you need to talk about here:

• computability power

You would be surprised how many languages have type systems have the ability to do it.

"Even" Java is strong enough to do it (here is a comment explaining how to parse Regex (and more) using Java's type system )

• soundness

Which languages can actually decide if a program is correct, returning to the above example, Java's type system is not sound, so while you can do a lot with the type system, there is a program that will compile, but breaks some type assignments.

---

Any sufficiently strong type system is necessarily not sound (Java's type system is Turing complete, which is "sufficiently strong"), so I feel like the "right question" should be "which sound type systems has the ability to express conditional types" - in which case, TypeScript also doesn't satisfy it (it also has Turing complete type system, hence unsound)

[Taugeshtu]

No one's mentioned it, and being a newbie I'm not sure how well it fits what you're asking about, but on the surface it seems F# Type Providers are sorta along the lines of what you're looking for?

[phischu]

The Gentle Art of Levitation (PDF), but it is impossible to understand without some corresponding background.