13

In my experience, all languages I know have a sort of "positive" type system. What I mean by "positive type system" is that when you are writing the source code, you always specify what types your function/objects accept, like:

function f(SomeType argument) { ... }

But I have never seen something like:

function f(AbstractType<Not ConcreteTypeFoo> argument) { ... }

I think it would be very useful in scenarios where you need to specify the behavior for some families of types without the need to write a lot of boilerplate code to implement some type exclusion logic.

By reading this wikipedia article abou type systems, I can see that maybe gradual type systems would be some sort of equivalent to this, but not exactly the same thing. I don`t think Union Types solve the same class of problem and saying that when you specify a type you are excluding other types is not the same thing as well.

// addition type system: argument can only be of type SomeType
function foo (SomeType argument) { ... }

// union types: argument can only be of type SomeType or FooType
function foo (SomeType | FooType argument) { ... }

// intersection types: argument must conform to both SomeType and FooType
function foo (SomeType & FooType argument) { ... }

// exclusion type: argument can be ANYTHING except ConcreteTypeFoo
function foo (AbstractType<Not ConcreteTypeFoo> argument) { ... }

An example scenario about where this would be useful:

interface Transaction() { ... }

class TransactionTypeA implements Transaction { ... }

class TransactionTypeB imnplements Transaction { ... }

class TransactionTypeC implements Transaction { ... }

interface TransactionRule() {
    boolean validate(Transaction t);
}

class RuleA implements TransactionRule {
    boolean validate(Transaction<Not TransactionTypeA> t) { ... }
    boolean validate(TransactionTypeA t) { ... }
}

class RuleB implements TransactionRule {
    boolean validate(Transaction<Not TransactionTypeB> t) { ... }
    boolean validate(TransactionTypeB t) { ... }
}

class RuleC implements TransactionRule {
    boolean validate(Transaction<Not TransactionTypeC> t) { ... }
    boolean validate(TransactionTypeC t) { ... }
}

The equivalent code without an exclusion type system would be like this:

interface Transaction() { ... }

class TransactionTypeA implements Transaction { ... }

class TransactionTypeB imnplements Transaction { ... }

class TransactionTypeC implements Transaction { ... }

interface TransactionRule() {
    boolean validate(Transaction t);
}

interface ValidationStrategy() {
    boolean validate(Transaction t);
}

interface ValidationStrategyFactory {
    ValidationStrategy create(Transaction t);
}

class RuleA implements TransactionRule {
    RuleAValidationStratetyFactory strategyFactory;

    constructor(RuleAValidationStratetyFactory f) {
        strategyFactory = f;
    }

    boolean validate(Transaction t) {
        ValidationStrategy s = strategyFactory.create(t);
        return s.validate();
    }
}

class RuleAValidationStratetyFactory implements ValidationStrategyFactory {
    ValidationStrategy create(Transaction t) {
        if (t.type == TransactionTypeA) {
            return new RuleATransactionTypeAValidationStrategy();
        } else {
            return new RuleATransactionTypeBAndCValidationStrategy();
        }
    }
}

class RuleATransactionTypeAValidationStrategy implements ValidationStrategy {
    boolean validate(Transaction t) { ... }
}

class RuleATransactionTypeBAndCValidationStrategy implements ValidationStrategy {
    boolean validate(Transaction t) { ... }
}

class RuleB implements TransactionRule {
    RuleBValidationStratetyFactory strategyFactory;

    constructor(RuleBValidationStratetyFactory f) {
        strategyFactory = f;
    }

    boolean validate(Transaction t) {
        ValidationStrategy s = strategyFactory.create(t);
        return s.validate();
    }
}

class RuleBValidationStratetyFactory implements ValidationStrategyFactory {
    ValidationStrategy create(Transaction t) {
        if (t.type == TransactionTypeA) {
            return new RuleBTransactionTypeBValidationStrategy();
        } else {
            return new RuleBTransactionTypeAAndCValidationStrategy();
        }
    }
}

class RuleBTransactionTypeBValidationStrategy implements ValidationStrategy {
    boolean validate(Transaction t) { ... }
}

class RuleBTransactionTypeAAndCValidationStrategy implements ValidationStrategy {
    boolean validate(Transaction t) { ... }
}

class RuleC implements TransactionRule {
    RuleCValidationStratetyFactory strategyFactory;

    constructor(RuleCValidationStratetyFactory f) {
        strategyFactory = f;
    }

    boolean validate(Transaction t) {
        ValidationStrategy s = strategyFactory.create(t);
        return s.validate();
    }
}

class RuleCValidationStratetyFactory implements ValidationStrategyFactory {
    ValidationStrategy create(Transaction t) {
        if (t.type == TransactionTypeA) {
            return new RuleCTransactionTypeCValidationStrategy();
        } else {
            return new RuleCTransactionTypeAAndBValidationStrategy();
        }
    }
}

class RuleCTransactionTypeCValidationStrategy implements ValidationStrategy {
    boolean validate(Transaction t) { ... }
}

class RuleCTransactionTypeAAndBValidationStrategy implements ValidationStrategy {
    boolean validate(Transaction t) { ... }
}

So, the question is: How can I simulate such scenario in a language like Java? It would be also helpful to get some background information of how this is solved in other programming languages.

21
  • 6
    { shrug } Anyone can ask a "does [some thing] exist" question, but that's not necessarily enough to make the question on-topic or demonstrate prior research. The best questions are the ones that are tied to a specific software design or development problem you are having. Feb 23, 2021 at 19:27
  • 3
    Also, when you say SomeType argument, you are already excluding all other types. Otherwise, you would just pass Object or somesuch. Feb 23, 2021 at 19:31
  • 2
    What you're describing is more of a negative declaration system, as opposed to the positive system of types we know. Negation is very hard to deal with mentally; consider that the NOR operator alone is as powerful as the normal AND/OR/NOT calculus, but there is a reason that no serious programing language uses that theoretically more elegant set-up. Feb 23, 2021 at 19:33
  • 3
    Your "Transaction," "Not Transaction" example is suggestive of pattern-matching. See here and here. Feb 23, 2021 at 20:43
  • 4
    How would you do anything useful with an exclusion type? A type tells you what a thing is, so you know what you can do with it. An exclusion type tells you what a thing isn't, so it tells you what you can't do with the ting - but that still means you don't know what you actually can do with it. I don't see how any implementation of your method would do any useful work. Also, any type kind of is an exclusion type already. FooBar is actually !(Everything \ FooBar)
    – Polygnome
    Feb 24, 2021 at 8:45

5 Answers 5

15

I'm not a logician, type theoretician, or programming language theorist, so my intuition may be wrong here, but I don't think it actually takes that much to be able to do this.

People have twisted Java's type system into quite some amazing shapes, for example. I would not at all be surprised to find out that what you want can be encoded in Java or similar languages.

I am also pretty sure that this is commonly used in C++ template metaprogramming. But I am not a C++ programmer either.

Such a type can be pretty easily encoded in Scala. One trick is to use implicits. It is illegal to have ambiguities during implicit resolution, so all you need to do is to write two implicits that become ambiguous IFF two types are equal. And that's really easy to do: you define one implicit for [A, B] and one for [A, A]. If the types are different, then only the first implicit is applicable and everything is peachy. If the types are equal, both implicits are applicable, and compilation fails with an ambiguous implicits error.

Here's what that looks like:

sealed class =!=[A, B]

trait LowerPriorityImplicits {
  /** do not call explicitly! */
  implicit def equal[A]: =!=[A, A] = sys.error("should not be called")
}

object =!= extends LowerPriorityImplicits {
  /** do not call explicitly! */
  implicit def nequal[A, B]: =!=[A, B] = new =!=[A, B]
}

This defines a type constructor named =!= with two type parameters A and B, which will lead to a compile error if you try to summon it with the same type. (Note that there is already a type constructor named =:= in the standard library which checks for equality.)

You could use it like this:

case class Foo[A, B](a: A, b: B)(implicit e: A =!= B)

This defines a type constructor Foo with two type parameters A and B which can only be instantiated when A and B are not equal:

Foo(1f, 1.0)
Foo("", 1.0)
Foo("", 1)
Foo("Fish", Some("Fish"))

// doesn't compile
Foo(1f, 1f)
// ambiguous implicit values:
//   both method equal in trait LowerPriorityImplicits of type [A]A =!= A
//   and method nequal in object =!= of type [A, B]A =!= B
//   match expected type Float =!= Float

Foo("", "")
// ambiguous implicit values:
//   both method equal in trait LowerPriorityImplicits of type [A]A =!= A
//   and method nequal in object =!= of type [A, B]A =!= B
//   match expected type String =!= String

But you can also use it this way:

case class NotInt[A](a: A)(implicit e: A =!= Int)

NotInt("")
NotInt(true)
NotInt(42f)

NotInt(42)
// ambiguous implicit values:
//   both method equal in trait LowerPriorityImplicits of type [A]A =!= A
//   and method nequal in object =!= of type [A, B]A =!= B
//   match expected type Int =!= Int

TypeScript can express powerful type constraints, since its type system tries to cover all the strange runtime tricks ECMAScript programmers pull. In particular, conditional types are very powerful, but there's also type guards, mapped types, distributive conditional types, and more. The TypeScript standard library actually already contains a utility type called Exclude<Type, ExcludedUnion> which gets you halfway to your goal.

Exclude allows you to create a new type by excluding a union of types from another type. Then, you can create another type which is the intersection of the exclude type and the parameter type. If the parameter type is one of the excluded types, then this intersection will be empty [Code inspired by an answer to Is there a type in TypeScript for anything except functions?]:

type NotA<A, T> = Exclude<T, A>

function noNumber<T>(notN: T & NotA<number, T>) { return notN; }

noNumber("Hello");

noNumber(2);
// Argument of type 'number' is not assignable to parameter of type 'never'.
2
  • 3
    Indeed, in C++ template meta programming it is common to write code that will not be instantiated for types with certain properties with a technique called SFINAE. It looks a bit similar to me to the Scala example except that it is, as the name says, not an error; instead, a viable fallback or alternative is chosen by the compiler. Feb 24, 2021 at 10:45
  • SFINAE was what I was thinking of, but I wasn't sure if that's actually what it was. Feb 25, 2021 at 23:03
4

I think that there are many languages that would support your TransactionRule usecase without "negative types", provided that they have some form of multimethods or pattern matching where a method matching a more-derived type receives a higher priority than a method matching a less-derived type. For example in Raku:

class Transaction { }

class TransactionTypeA is Transaction { }

class TransactionTypeB is Transaction { }

role TransactionRule {
  method validate(Transaction --> Bool) { ... }
}

class RuleA does TransactionRule {
  proto method validate(Transaction $t --> Bool) {*}
  multi method validate(TransactionTypeA $t --> Bool) { True }
  multi method validate(Transaction $t --> Bool ) { False }
} 

my RuleA $rule .= new;
say $rule.validate(TransactionTypeA.new);
say $rule.validate(TransactionTypeB.new);

which prints True False because multi method validate(TransactionTypeA --> Bool) catches objects of that type while multi method validate(Transaction --> Bool) gets the remainder. The proto isn't entirely necessary but enforces that you don't write validate methods that accept non-Transaction objects, which seems within the spirit of your example.

(incidentally, the { ... } in the role is literal syntax: a body of ... declares a "stub", and providing stubbed methods in roles is how you declare that any class consuming the role must provide an implementation for that method, a la interfaces).

2

C++ has this kind of thing in various forms:

In, C++20 using shorthand function template syntax, calling this function with something that satisfies the std::is_integral_v type trait gives you a static assertion error:

void f(auto not_a_number)
{
  static_assert(!std::is_integral_v<decltype(not_a_number)>);
}

See it live on godbolt. An alternative (but I don't think an entirely equivalent) way I can think of doing this:

auto f(auto not_a_number)
 -> std::enable_if_t<!std::is_integral_v<decltype(not_a_number)>>
{
}

You can tell the compiler error is more nasty this way, live on godbolt.

Or if you prefer the old explicit template syntax:

template<typename T>
void f(T not_a_number)
{
  static_assert(!std::is_integral_v<decltype(not_a_number)>);
}

Which is equivalent to the first option.

Note these "negative type system" strategies are usually applied to limit the "positive type system" more general variants/overloads/implementations of something, or provide a specialized implementation when a condition (not negative per se) is met.

-1

The are programming languages out there where the type system allows for these sorts of constructions.

Typescript Scala

They just aren't common because it is hard to operate on the absence of fields but they make useful generic type constraints in some circumstances.

2
  • 1
    can you show some example?
    – user218158
    Feb 23, 2021 at 19:28
  • I was pretty sure Typescript had something similar (I'm very far from fluent in Typescript), so I followed the Typescript link above to an SO page that described some examples.
    – Flydog57
    Feb 24, 2021 at 5:21
-1

Kind of. I'll try to keep this answer simple without jargon or needless details.

You can think of negation as a label/continuation. A proposition and it's negation leads to explosion. And indeed a continuation and it's parameter can jump out of any context.

A limited form of continuations are exceptions which can be thought of as dynamically scoped continuations.

I should note combining coexponentials and exponentials (gibble gabble for continuations and higher order functions) without restraints breaks purity and makes the order of evaluation matter.

There are many languages that have limited support for continuations but in general they are poorly studied as a practical thing. From a type theory perspective coexponentials are exactly dual to exponentials and also mutually exclusive (without restraints like linear types) and so don't get enough love. IMO they are underappreciated.

Anyway, I don't think any languages implement quite the sort of thing you are discussing. But I would feel the foundation of any system of negative types would in some sense involve continuations/coexponentials.

1
  • 2
    Hey Molossus. Thank you so much for your response. Unfurtunately, I couldn't quite understand anything of what you tried to say, hahah.
    – user218158
    Feb 24, 2021 at 1:47