Types and values

This originally came out of a discussion (more of a rant) by me on an IRC channel. The original text (with intermediate stuff stripped) can be found at the bottom.

The questions I’m trying to answer are “What are types? How are they practically useful?”. I’ll start by making some comparisons to Python and Haskell.

Python is my classic example of a language that’s not typed. Granted that’s a lie, as it’s dynamically typed, not untyped, but please ignore my terrible misuse of terminology and just go with me. For example, let’s say we have a function. Looking only at its signature, what can you tell me about it? No cheating by looking at argument names or similar things, essentially, we’re the compiler (and the compiler doesn’t know English words). Practically, you can tell me almost nothing. Perhaps you can assert it takes two arguments and might return a value (in this particular case).

Let’s move on to Haskell. Say this function has the type (Num a) => a -> a -> a. Woah! We can suddenly say a lot about what the function does! It takes two arguments (well, curried) and returns one, all three the same type. The Num constraint also implies we’re doing something mathematical to it, maybe adding, or multiplying the two arguments. We could do something dumb, too, like make it just be implemented by the const function (discard one argument and return the other). Look at how there’s a few different possible implementations: there’s quite a lot of specificity in the type (more so than Python!), but there’s still room for different or odd implementations.

Taking a step back, let’s look at the Haskell tool Djinn. I haven’t used it much, but from what I understand it, it takes a type, and attempts to find a function/value that will satisfy that type. It can do some pretty complicated things, too! When given (a -> b) -> (a, c) -> (b, c), it gives back f a (b, c) = (a b, c) (which is pretty simple, but you get the idea)! However, note that because of my previous comments about Haskell having room for different implementations, Djinn cannot be perfect and implement any type thrown at it.

But… let’s stretch our imaginations for a bit, and enter the land of hypothetical situations. Imagine a new language, let’s call it SuperTyped, whose types allow for one (and no more than one) implementation (and maybe zero implementations). Return to the two-argument function example from earlier. Say, the syntax for the type was something like (a, a) -> <type whose value is sum of first argument>. Granted, the compiler would have to be pretty magical to figure that out, but this is imagination-land. Then, say a Djinn-clone was made for this language. We would no longer have to write any function implementations! Just embed the Djinn-clone into the compiler, and have it generate the function for you.

Wait a minute. Didn’t we just shove the “implementation” of the function into the type? Pretty much, yeah. So here I start making leaping conclusions: Types are useless without an underlying value system that is more expressive than the types themselves. If there exists only one (or zero) implementations of a type, as in SuperTyped’s Djinn, then we might as well be writing in an untyped language. If the types are the implementation, we just wrote def f(x, y): return x + y but called it a “type”, no better than that code as Python.

Exploring that idea more, we come across the idea that typechecking is evaluation in SuperTyped. So wait… apparently, then, running a Python program is equivalent to typechecking it. This makes sense! If a TypeError is raised (or some other exception), then obviously the program is badly typed. But there’s a difference here - typechecking is usually done at compile-time, and evaluation is usually done at runtime. So let’s restate the previous statement about types being useless, but with slightly different words. Types are only useful if they can be checked at compile-time, even if their values cannot be obtained until runtime. IO is a perfect example of this. The value of an IO in Haskell cannot be obtained until runtime, but its type can be checked at compile-time. Again, though, there’s this looseness of “the compiler cannot fully check it until runtime”, with, for example, malformed input.

Restating that final paragraph as a final conclusion: The reason types are useful is that they can be evaluated (and checked) when the value that holds that type cannot be obtained at that moment.

Thanks for reading! If you happen to know any more formal research related to this topic, I’d love to read about it! This was done entirely from my own ideas, so I’d love to read some peer-reviewed things to clarify the probable holes my arguments have, etc., and maybe edit this article to fix them. And, as I mentioned in the introduction, this was originally a text barf on IRC, which the log can be found below.

17:54 <khyperia> .... wait a minute, I just had a serious language design
    lightbulb go off
17:57 <khyperia> so there exist tools in haskell that do things like "given
    a function signature, attempt to make an implementation for the
    function". It doesn't always work due to lack of information on what the
    function does in the type (but seeing as it's pretty strongly typed, it
    does alright). So that got me thinking: design a language that exists in
    source solely in types, and the compiler always can figure out how to
    implement a function. Then I realized: this is pretty much practically
    equivalent to an untyped language, we just changed the meaning of a few
    things, and poof. So my lightbulb: Typing isn't useful just due to
    typing. It's useful because there's a value<->type relationship.
17:58 <(not me)> properly typed programs are properly typed
17:59 <khyperia> I'm more talking about the strength of types, and what
    guarantees the type makes about the behavior of a function
18:00 <khyperia> it ranges anywhere from python ("it doesn't tell you
    anything"), to haskell ("lots of stuff, but not everything"), to my
    hypothetical language ("everything is specified in the type")
18:01 <khyperia> for example, the haskell type "(Num a) => a -> a -> a".
    This could be anything, really, but we know it probably involves math of
    somesort as a binary operation. If we change that to"(Num a) => a -> a
    -> <type indicating that it's the sum of the first two args>", then we
    know exactly what the function does.
18:02 <khyperia> and in the hypothetical language, the actual implementation
    isn't needed to be typed out, because the compiler can infer it
18:02 <(not me)> seems like you just kicked the buck down to that last type
18:02 <khyperia> ... but wtf, we basically just typed it out in the type
    instead, "x: a -> y: a -> (sum of x and y): a"
18:03 <(not me)> ye, and the compiler has to know what sum means
18:03 <khyperia> yeah, stuff like that, etc., but assume it's a fancy
    compiler. (Idris compiler does something similar)
18:04 <khyperia> so taking a big leap, I say that writing it in the type is
    no different than writing the function itself.
18:04 <khyperia> so therefore types as types themselves are useless, and
    need an underlying value that's more specific than the type to be useful.
18:08 <khyperia> Or, in other words, when given a program, why not just
    evaluate it to see if it's right? If it all typechecks / runs correctly
    (identical under my theoretical language), then happiness!... which
    putting it in those words, makes it more clear: types are useful because
    they describe the behavior of a value when there's no value present to
    check against (for example, it comes from IO)
18:08 <khyperia> Hmm. That's enough ranting for me, I'm going to go throw
    this in a blog post since I feel like it's super interesting.