[theory] What is a type?

[Mark]

On Sunday, 10 October 2010 at 12:28:32 UTC, Justin Johansson 
wrote:
> Specifically I have a problem in trying to implement
> a functional language translator in D.  My target language
> has a rather non-conventional type system, in which,
> superficially at least, types can be described as being
> Cartesian in nature. That is,
> types in this system have two orthogonal dimensions:
> (1) classical data-type (e.g. boolean, number, string,
> object) and
> (2) Kleene cardinality (occurrences) with respect to (1).
>
> The axial origin of this Cartesian type-system correlates well
> with the concept of the "top" type (AKA "Unit" in Scala)
> and as the rather adhoc "void" type in many Algol-derived
> languages such as C/C++/Java/D.
>
> So along axis 1 we might broadly describe the classical
> data types as item, boolean, number, string, object where
> item is effectively either a superclass or variant of the
> other mentioned types.
>
> Along axis 2 we describe Kleene occurrences of 1 as may be
> passed contractually to a receiving function.  These
> occurrences may be enumerated six-fold as:
> zeroOrMore
> zeroOrOne
> oneOrMore
> exactlyZero
> exactlyOne
> none
>
> Readers may see that, for example, zeroOrOne is a special
> case (perhaps a subclass?) of zeroOrMore.  exactlyOne is
> a special case of both zeroOrOne and oneOrMore (sounds like
> multiple inheritance?).  OTOH, exactlyZero is a special
> case of zeroOrOne, which, in turn, is a special case of
> zeroOrmore.
>
> none is a special case of all of the above and reflects
> the cardinality facet of the return type of a function
> that never returns (say as by throwing an exception).
>
> To make this type system even more enigmatic lets add a
> third dimension, taking the 2-D Cartesian type system
> model to a 3-D Spatial model, by imagining a further
> degree of freedom with respect to laziness of evaluation
> (AKA closure of arguments).
>
> Now having hopefully described that a type is something
> that might well have multiple orthogonal aspects to its
> identity, how would one go about implementing a dynamic
> language with such a complex type system in D?
>
> I realize that this is a complex topic and that it might
> require better articulation than so far I have given.
>
> Nevertheless, thanks for all replies,
> Justin Johansson

Well, in D-speak you could imagine taking (perhaps arbitrarily) 
the first axis (basic data type) as the "skeleton" and attach 
various properties to it. For example:

Int!(exactlyOne, eager) x = 42;
Int!(zeroOrMore, lazy) y;
readf("%d", &y);
auto foo = x+y; // What does this mean? What type is foo?

You seem to have in mind a syntax for your type system but I'm 
not sure how you intend for the semantics to work. D's templates 
are really nice in that they allow you to express many properties 
of a term that are not "hard coded" into its type. So you can do 
stuff like:

enum MinimizationTarget { programThroughput, GCThroughput, 
heapOverhead, pauseTimes, pauseFrequency, heapFragmentation, 
warmupTime }
auto GarbageCollector(MinimizationTarget[] priorities = [])()
{
     static if (priorities == []) return 
StopTheWorldMarkAndSweepGC();
     else static if (priorities[0] == heapFragmentation) return 
copyingGC();
     else static if (/* some boolean algebra condition on 
$priorities */) return GenerationalMarkAndSweepGC();
     else /* etc. */
}
auto myGC = GarbageCollector![pauseTimes, heapOverHead, 
programThroughput];
auto myGraph = Graph!(myGC, directed);

which is pretty cool. :)