Once again, I am looking for examples of languages implementing a given feature. Today, the feature I'm looking for is about representing types as predicates. So, a type is actually a function that takes any object as an argument, and returns true if and only if the object is of that type. For example: 10 : int is true true : int is false int : any -> bool is true (it's a predicate). (As a notation, type := any -> bool;) And so, the language provides built-in predicates corresponding to the basic types (integers, booleans, functions, null) and allows the creation of new predicates. For example, we can define the type of elements that are even integers, or positive integers: def even(x:any) = (x:int) && (x%2==0); def positive(x:any) = (x:int) && (x>=0); By overloading boolean operators for predicates (def (a && b)(x) = a(x) && b(x);) we immediately have access to a subset of algebraic types: def animal = cat || dog; def positive_even = positive && even; def odd = int && !even; Even better, we have access to dependent types by using partial applications (in my example, currying): def multiple(n:int)(x:any) = (x:int) && (x%n==0); def option(x:type) = x || null; This allows an interesting elegance to the null approach: assert(x: !null); Last but not least, we can allow any set definition, by using undecidability to hide away pasky definition problems. Cantor would play out as: def cantor(e:any) = (e:type) && (e: !e); So cantor:cantor would turn into an infinite loop. So, do any of you have any references to languages that already implement this kind of things?

I think ML (meta language) is best for your requirement,
http://www.smlnj.org/ is a implementation of ML.

ML is a functional & imperative programming language, support built-in function pattern match, strong type, type inference, and can implement infinate list via functional programming.

C# provides the is operator, which tests if a given variable can be meaningfully converted to a type. We can write our actual predicate like so:

public bool TypePredicate<T>( object value ){    return value is T;}

This matches the signature for the Predicate<T> delegate type (aka function signature) provided by the framework and understood by a number of built in functions. And of course, we can use it ourselves as we please. You could also define And, Or, etc, but the syntax does get kind of akward (you'll end up with things like new AndPredicate( TypePredicate, OtherPredicate ), not to mention there's a type predicate implicit in something like EvenPredicate which makes things weird too).

Quote:Original post by lexchou
I think ML (meta language) is best for your requirement,

Not really. Most ML languages (and SML in particular) do not support types as first-class citizens (as a consequence of strong typing). In particular, in my example above, 0 would be of types "int", "positive", "even" and "positive_even", and only "int" in ML.

Quote:Original post by Promit
C# provides the is operator, which tests if a given variable can be meaningfully converted to a type. We can write our actual predicate like so:

C# does support the "Type => Predicate" approach (just like any language with reflection), but I was rather looking for the reverse "Predicate => Type" approach. Such as being to create a type that represents even integers, and use it as an actual type. I guess this would be possible as well using reflection, but I think it would quickly get out of hand.

Quote:Original post by
Common Lisp has something similar:
deftype and satifies

Yep, this looks like it. Although it doesn't really seem central to the language (Lisp does not do much in the way of types, as far as I've noticed).

After searching a bit more, it seems that Dylan implements a limited version of this, and so does Maple.

Quote:Original post by Rebooted
This is just dependent typing, but you need some form of subtyping too. I was implementing a type system like this, based on the ideas discussed here, from the Ontic language. I didn't really like the results though. I now think extending the ML type system is the way to go, so in that argument I'd say I side with Frank, not Tim Sweeney.

Subtyping is automatic: when a predicate A implies a predicate B, then A is a subtype of B by definition. Once could then decide to use a predicate such as "has method F of type [...]" to perform the checks.

This link is very informative, although on the subject at hand I'd side with Tim, and not Frank. My intent is to use types to enforce contracts. For example:

nonzero(i:any) = (i:int) && (i!=0);
divide(i:int,j:nonzero) = i/j;

The behaviour would be to cause a compile-time type error if divide was called on an object that could potentially be zero. So, the program writer would have to write a program which proved that j is nonzero, or to place an assertion stating assert(j:nonzero); before the call, or to handle the cases differently using an if(j:nonzero) {...} else {...}.

So, in a way, I'm looking at types as sets of objects which have a certain property, which I can then use to detect errors at compile-time, and express contracts in a nicer way than a few words in the documentation and a bunch of asserts at the beginning of the function. Which is why type-checking was introduced in the first place, after all...

Quote:The closest I'm aware you can get to this at the moment is in a dependently-typed language such as Epigram, or a theorem prover like Coq. I think I've heard that Lego has (coercive) subtyping, which might get you what you want.

I've already looked at Epigram and Coq, but they take a rule-based proof approach to the deal, while I'm going for a simpler "a type is a predicate" idea (which still relies on proofs, but will be easier to evaluate). I haven't looked at Lego yet.