2

I am brain storming on how to create a type system for a programming language, and what the compiler will do with the typing information. Here is what I have found, followed by the main question, which is if I can represent more complicated "validations" as types somehow.

First, it seems there is a difference between the physical record structure of an object stored in memory, and a "type". An object for example can be "typed" such that it is either an odd fibonacci number, or an email formatted string, let's say. That is its "type" in some theoretical type system. But the physical record is either an integer or a string, which have actual ramifications on the physical memory. It's like there is a "data type", and a "validation type".

Given that, a traditional "type" ("validation type") is really a set of constraints over the underlying data type(s). Since it can be over many data types (integer or string in the last example), it is really over an abstract data type which encompasses all data types, the "base" data type. Then on top of this base data type, which is some sort of in-memory record, you have a set of constraints. These constraints can be over individual record fields, or over several fields in the record. The constraints are boolean-resolving functions.

But this poses a problem for "inspecting the type". If we want to see the type for our "odd fibonacci number or email string" object, and it is stored as a set of constraints (isOdd, isFibonacci, or isEmail), then you have to inspect these constraint functions to determine the type. But these functions would be useful for a type-checker, because the type-checker could check all the constraints of the type somehow and use them to infer other types or do typechecking (haven't gotten this far to know how it's implemented yet). Ideally, too, they would be useful for a compile-time type checker, a static type checker.

You could take the boolean constraint functions further so they are extremely complex async processes which run to determine if the data structure is the correct type. For example, say we had a type "if it's a full moon then set the time to midnight, otherwise set the time to regular time". Something crazy. Then it would make an HTTP request (a non-boolean function) to determine the full-moon status, and then check the value based on that status. There can be all kinds of async non-boolean functions embedded into the ultimate "boolean" constraint function, that it is hard to tease them apart and build a DSL that is "only boolean logic functions". When you get into practice, the line between a pure boolean logic function and just an imperative function or set of assembly instructions starts to blur.

So a "type" is really a set of constraints on some underlying data type in memory so to speak.

With this in mind, can all of these sorts of things be done at compile time? I don't think the moon example could be done, it seems some types will have to be checked at runtime dynamically. So then, what are the types of type-checking that can be done statically?

Are languages like Haskell or Coq able to somehow solve this problem of resolving these constraints at compile time? Or is there a fundamental limit to how far type systems can take you? I would like to do as much static compile-time type checking in a custom programming language as possible. But I keep thinking of these complex async function examples of constraints that might pop up in a "type", and it throws the whole system off. I feel like types must be severely restricted and limited in what they can do, and everything else must be done at runtime. But I'm not sure.

4
  • 1
    There really is no limit other than the amount of information the compiler is given in advance. For an example of type system that can go to both extremes: Magpie Type checking is a form of partial-evaluation. It can extend so far as to fully evaluate the system (such as C++ templates), or do nothing upfront at all (like many scripting languages).
    – Kain0_0
    Commented Feb 28, 2021 at 3:42
  • 3
    "is there a fundamental limit to how far type systems can take you" yes. If it's a general purpose programming language though, compile times are probably going to be your main obstacle. It's incredibly frustrating for line-of-business programmers to have to wait 20+ minutes to see the impact of a change. "What you can verify at compile time" quickly degrades to "what you can verify at compile time in a reasonable amount of time". Commented Feb 28, 2021 at 11:36
  • @JaredSmith can you provide some more examples of cases where it degrades your experience? I can imagine perhaps model checking taking too long, but don't know much else.
    – Lance
    Commented Feb 28, 2021 at 13:51
  • 1
    @LancePollard that's a can of worms I don't want to go to deep into, but consider this: type-checking is only one facet of one phase of compilation. So it's not just that "the type-checker takes too long". The average Joe/Jane is not going to dig that deep into compiler internals, they just know that their life sucks because correcting a typo takes 20 minutes to recompile. Some languages (e.g. C++) are hard to parse, some build systems are rough (e.g. Java on Android), some languages require recompiling linked modules (C++ again). So the type checker also frequently has to compete for budget. Commented Feb 28, 2021 at 16:22

3 Answers 3

3

Yes, types are just constraints. Any general type system has top which means “this value can be anything” and bot (bottom) which is so constrained that no value can satisfy it.

That’s literally chapter one of any type theory book.

What can be determined at compile time depends on your operations. isEmail is trivial if you only allow constants in your language. It gets a little more complex when you allow concatenation. Once you allow casting (or I/O) then your compile time typechecking can no longer prevent all runtime errors.

isFib is pretty simple until you allow addition, while isOdd remains pretty simple.

Haskell and Coq especially can do more at compile time because they’re specifically crafted to limit the things that are only provable at runtime.

2

You might want to look into refinement types, which are types with programmer-specified restrictions along the sort you mentioned.

The main thing that determines if you don't need a runtime check is if you are casting from a subtype to a parent type. fibonacci is a subtype of int, for example, so a cast from fibonacci to int can be safely done without a runtime check.

A cast in the other direction requires a runtime check because there are some ints that are not fibonaccis. This is really no different than a conversion from string to int.

0

The concept of a "type" is really a human concept, over and above anything that corresponds to any physical implementation. When a programmer says that a variable is of type color, with values such as red, green, and blue, he is trying to describe a constraint that can be detected and therefore enforced by the programming language. He really doesn't care that the physical implementation consists of integers ... he's saying that the variable "is a" color, and he wants the language to enforce that.

For example, the statement i = red can be objectively recognized to be an error if "the type of" i is not color. In other words, "the programming language found this bug for you." (Whereas, you, poring through mountains of source-code, probably never would. "Being a digital computer has its advantages ...")

Static typing takes place "at compile time." If you violate one of these rules, your program "doesn't compile."

Dynamic typing relies upon at-runtime checks, which are probably performed by a language interpreter. Purely-interpreted languages have no concept of "compile time," and support situations that are entirely transient ... possibly created by [vast quantities of ...] source-code that your program knows nothing of. Dynamic typing is the only mechanism that such languages can use. Type-related checks occur constantly at runtime, and this overhead is judged to be acceptable.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.