Hacker News Reader

Comment by TeMPOraL | Hacker News Reader

One thing I wish for is some kind of "type tags". Being able to express concepts like List[Widget], List[Widget, Nonempty], List[Widget, Nonempty, Sorted], Vector[User, Sorted], etc. - or even, more generic, <Container>[<T>, NonEmpty] (where <Container> and <T> are parameters, like in C++ templates) - without implementing an explicit new type for each. Logic verification through typing would then involve not just changing "main" types, but also adding and dropping "tags" from the "set of tags" attached to the "main" type. This should cut down on the amount of boilerplate.

Hell, in the extreme, perhaps types in general could be generalized as a set of tags?

View on HN

This is quite similar to units (e.g. F# units of measure) or taints (Perl, for tracing user input and detecting unsafe usage).

A large part of the point of these systems is that you can write code which generalizes across the different subtypes (different units, tainted vs untainted values) yet it still passes through invariants by default (values calculated from tainted input are themselves tainted, a unit-quantified value multiplied by a scalar retains its unit, and so on).

I've done similar things with syntax trees in compilers. With multiple passes, you have a representation for the output of the parser, then you might do type annotation, rewrites due to coercion etc., symbol binding and overload resolution, constant expression evaluation, and so on in separate passes. If the input and output trees for each pass have different types, it's easier to keep track of what's going on, of what invariants hold for any given tree node, or indeed which node types are permissible to exist in the input or output of a pass (e.g. you don't want unbound overload calls after overload resolution).

One problem is that tags probably aren't enough when you're dealing with data structures rather than simple zero-dimensional values. Some methods shouldn't be called, or some fields shouldn't be accessed, if a value has a type with the wrong tag. But if you have a wholly different type, then you can end up reimplementing a lot of the same logic, once per type, simply to get the types to flow through.

One solution I've used a couple of times for the tree problem is tree grammars. That is, a data structure which encodes a description of a valid tree and can encode invariants like nodes of type T need to have attributes of type Y with values satisfying predicate P, and between N and M children of type U, V or W, and so on. The grammar is defined in terms of an abstract supertype, and the concrete subtypes have the grammar specific to their phase baked in. This is a hybrid between static and dynamic typing, a compromise necessary for languages like Java without much expressiveness in the type domain.

When you have higher-kinded types you can build that kind of thing yourself. Dependent types going further in that direction. Take a look at Idris.

I will, thanks. I never had a chance to catch up on the "state of the art" in typing systems.

I'm not even sure if my "types as a set of tags" idea makes much sense - perhaps it decays to what is typically understood as types. Or perhaps it hits computability problems.

I did some mental experiments on a "set of tags" type system last night, and I quickly realized the complexity will be around deciding when to keep a tag (property) on a type, and when to drop it. With a set of tags being open, a function could not possibly know about them. This creates a problem.

Consider a function like: Sort([List[T], ...], [Function([T, T] -> Bool)]) -> [List[T], Sorted, ...]. Takes a list and a comparator, sorts the list, attaches a "Sorted" tag to return type, retains all other tags. Looks like a reasonable definition. Let's look at the use cases below (with P being some applicable predicate):

- Sort([List[Int], P) -> [List[Int], Sorted] -- OK!

- Sort([List[Int], NonEmpty], P) -> [List[Int] Sorted, NonEmpty] -- Awesome, exactly what I want!

- Sort([List[Int], Foobar], P) -> ...? Should it be [List[Int], Sorted, Foobar]? But what if Foobar designates some business rule that depends on the element ordering? How is Sort supposed to know?

Without knowing a tag, we'd sometimes want a function to drop it, and other times want the function to retain it. I have no idea how to solve this at compile time (or even at runtime, without crippling the tagging system).

Would it be ok if you could define relations between tags in code integrating them?

    Contradicts sorted foobar
    Independent sorted nonempty
    Independent foobar nonempty

Additionally there should be tag that contradicts everything by default.

A language like Kotlin can do some of these things using delegates, interfaces and extension methods.

For example a MutableList<T> can be dropped down to a List<T> which is not mutable. And a generic conversion from Collection<T> to NonEmptyCollection<T> should be trivial to write as an extension method.

Can Kotlin handle multiple "tags" on a type as a set, and not a sequence? I'm not familiar with the language, so I'll use a C++ analogy. If you tried to tag types in C++, you'd end up with something like:

  TaggedType<std::vector, NonEmpty, Sorted>

but such type is strictly not the same as:

  TaggedType<std::vector, Sorted, NonEmpty>

What I mean by "set" instead of a "sequence" is to have the two lines above represent the same type, i.e. the order of tags should not matter.

You can maybe get there in kotlin with a generic type with multiple constraints in a where clause. Let’s say you have Sorted and NonEmpty as interfaces (could be empty marker interfaces so they behave like tags). Then you can write a method

  fun <T> doSomething(values: T) where T: Sorted, T: NonEmpty {}

And that function will take any type that has both Sorted and NonEmpty interfaces.

You don't need Kotlin to do this, even Java can do it:

    <T extends Sorted & NonEmpty> void doSomething(T values)

Reply on news.ycombinator.com