I have been puzzling this a while.
In Ocaml (and Felix) a union has two kinds of constructors:
union list = Empty | Cons of int * list;
Cons is your normal constructor taking arguments, its called a non-const
constructor because Empty is a constructor taking no arguments and
is called a const constructor.
In ATS, there are no const constructors as such. Instead, ATS insist on this:
union list = Empty of unit | Cons of list * int;
which means one writes an empty list like so:
var x = Empty ();
"In principle" a constant constructor is nonsense. But I'm disturbed because it
works. Some how we have confused a value with a function.
Now we know a function like this:
fun one () => 1;
is a constant function, without looking at the implementation, since it has
only a single valued argument all calls have to returns the same result.
There are other constant functions, such as:
fun one (x:int) => 1;
but here you need to look at the implementation.
But what is 1? In a categorical model, there are no values ONLY functions.
But if we write 1, what kind of function is it?
It has no arguments so we'd be tempted to say:
1: 0 -> int
The advantage of this idea is that 1 cannot be applied to anything,
but it doesn't matter. You can still add two such functions together
to get
2: 0 -> int
Note here 1 and 2 function names are integers not types!
There is a problem though. In a distributive category, there can be
at most one initial object. In the category of sets and functions,
which is the denotational interpretation of a type system,
there is a single void type, namely the empty set
{}
Now recall with sets a function can be modelled by a set of pairs.
Note: its a MODEL of a function, not the actual function.
A function:
f: {} -> T
is modelled by set of pairs of values from the domain {} and codomain T,
and such a set certainly exists .. and is empty of any values. The point is
that this function really does exist, and in particular it is unique. There can
only be ONE function from the empty set to any given set T. So in fact,
that function *characterises* the set T: for every T there is exactly
one function
0 -> T
So now, we're back to the question what is 1? It cannot be:
1: 0 -> int
because we would also have
2: 0 -> int
and that would mean 1 = 2 :)
The ANSWER comes from ATS:
1 : 0 -> int(1)
The codomain called a singleton type. It is a subtype of int,
consisting of exactly one value (in this case, the value 1):
{1}
Such dependent types are the way to get "dependencies" into
the type system.
But now, I know what 1 is: its a function from 0 as I thought but
the domain is a singleton subtype of int (not int).
--
john skaller
skal...@users.sourceforge.net
http://felix-lang.org
------------------------------------------------------------------------------
LIMITED TIME SALE - Full Year of Microsoft Training For Just $49.99!
1,500+ hours of tutorials including VisualStudio 2012, Windows 8, SharePoint
2013, SQL 2012, MVC 4, more. BEST VALUE: New Multi-Library Power Pack includes
Mobile, Cloud, Java, and UX Design. Lowest price ever! Ends 9/22/13.
http://pubads.g.doubleclick.net/gampad/clk?id=64545871&iu=/4140/ostg.clktrk
_______________________________________________
Felix-language mailing list
Felix-language@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/felix-language
