Not My Type
Not My Type, named after its lack of actually being a type based language, yet still "claiming" to be, is an esoteric programming language created by User:Yayimhere, based on the N -> (N -> N) type notation.
Definition
Not My Type uses two types of objects. Types, and Creators. A Type, acting like a function, has one or more definitions, written as x -> y(left associative). This definition defines the case when an object has been given as input, of type x, and what will be returned. x may be referenced in y, however this technically will reference the type, and not the object itself(though in most cases, the type just holds itself). All but one type hold only themselves. The exception is v, which holds all objects, and has the diagram x -> v. There are is one primitive type, M, which is defined as M : v -> M(note the syntax). Now onto creators. Creators take a single input, and create a type from it. There are two primitive creators, l(x), and N(x). These are defined as l(x) : x -> x, and N(x) : M -> (l(x)). Application of both types and creators is written as F(x), while also allowing brackets. Objects can be defined by the programmer, either simply labels for other values, type definitions, or creators, given as follows:
Name : Expr Name : Typedef Name arg : Typedef
(these may only recurse on the left side of an arrow). Every line is a definition like this. Only the things specified, are what makes up programs. Also, creators are also types holding all the types they can define(which technically is another excetption to the condition from before). When naming a creator as a type, its name is simply used without any input or application. Here is an example of a simple program:
T x : T -> x n : T -> M n : M -> T
as you can see, a type/creator can have multiple definitions for different cases. The above type defined n, works as a sort of Lambda calculus style NOT.
Example
P x : x -> (x(x))(x) (P(P))P