dotty type support | and & but not support not type like !T

[eagoo]

because | & add ! type compo can combine describe all types in the world

[liufengyun]

It's not clear what you mean by "all types in the world"? How can you represent function types with |, & and !?

In intuitionistic type theory, "!T" is interpreted as T => False, where False is a type with 0 constructors. In Scala, you can think !T is T => Nothing. This is useful in theorem provers like Coq, but I don't see how it's useful in practical programming.

[eagoo]

now using scala type check not a type implement can use T (implicit ev: T =!= SomeType)
when compile like T =:= SomeType
i think dotty should impl ! type directly without using implicit param check hack

[liufengyun]

Ah, I get what you mean -- you want to interpret X & !T as (X, X =!= T). Generalising that usage into a new type !T seems possible, though it complicates the type system.

[liufengyun]

By using implicit function types, the boilerplate with type equality and inequality(when supported) evidence can be avoided:

type ~[U, C] = implicit C => U

def f[T](x: T): Int ~ (T =:= Int) = 3

If this addresses your concern, then it doesn't justify to complicate the type system by introducing another language level type operator.

[eagoo]

i can not catch implicit function types mean
could it implement

trait Animal
trait Dog extends Animal
trait Cat extends Animal
trait Chick extends Animal
//... ...
//here i just want x type is a not dog animal
var x : Animal & !Dog  = new Cat{}

[odersky]

This needs much more than a spec. We need some breakthroughs in type theory to make this happen. So let's wait until we see this in actual CS textbooks before we reopen this issue ;-)