How can I simulate a "negative" type system?

Question

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.

{ 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. — Robert Harvey
– Robert Harvey, Commented Feb 23, 2021 at 19:27
Also, when you say SomeType argument, you are already excluding all other types. Otherwise, you would just pass Object or somesuch. — Robert Harvey
– Robert Harvey, Commented Feb 23, 2021 at 19:31
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. — Kilian Foth
– Kilian Foth, Commented Feb 23, 2021 at 19:33
Your "Transaction," "Not Transaction" example is suggestive of pattern-matching. See here and here. — Robert Harvey
– Robert Harvey, Commented Feb 23, 2021 at 20:43
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
– Polygnome, Commented Feb 24, 2021 at 8:45

Jörg W Mittag · Accepted Answer · 2021-02-23 20:21:13Z

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'.

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. — Peter - Reinstate Monica
– Peter - Reinstate Monica, Commented 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. — Jörg W Mittag
– Jörg W Mittag, Commented Feb 25, 2021 at 23:03

hobbs · Accepted Answer · 2021-02-24 07:03:26Z

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

rubenvb · Accepted Answer · 2021-02-24 10:41:04Z

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.

Sign · Accepted Answer · 2021-02-23 19:24:27Z

-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.

answered Feb 23, 2021 at 19:24

Sign

2,73321 silver badges22 bronze badges

1

can you show some example?

user218158
– user218158

2021-02-23 19:28:46 +00:00
Commented 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
– Flydog57

2021-02-24 05:21:12 +00:00
Commented Feb 24, 2021 at 5:21

Add a comment |

Stack Exchange Network

How can I simulate a "negative" type system?

4 Answers 4

Hot Network Questions

How can I simulate a "negative" type system?

4 Answers 4

Related

Hot Network Questions