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], 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).
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).