On 08/13/2011 07:10 AM, Yrogirg wrote:
Back to the initial question. Does first-class object types mean the
same as dependent types? In that case there is a wikipedia article
http://en.wikipedia.org/wiki/Dependent_types that can serve (at least
for me) as a starting point for the answer.
No, it's not the same.
Dependent type means that the type depends on a value.
For example, write a function that given a positive integer returns a
zero vector of size n. Of course, you can construct its function type by
zero: PositiveInteger -> Vector(Fraction Integer)
where Vector would be the domain of arbitrarily long vectors
(mathematicaly speaking the "union of all finite vector spaces over
rational numbers". That is *not* a dependent type.
Now suppose, you really want to separate all those types, i.e. something
like Vector(n, Fraction Integer) for a given dimension n.
Then you would have
zero: PositiveInteger -> Vector(n, Fraction Integer)
But hey, what exactly is the return type? The n is not specified in the
above signature. Exactly for that reason the above type is not possible
in SPAD and you'd have to write
zero: (n: PositiveInteger) -> Vector(n, Fraction Integer)
And, voila. You have a dependent type. Vector(n,Fraction Integer)
depends on the n that is given as input to the function zero.
In some sense the result type is not static. Since the exact type is
only constructed at runtime.
And now, "first class"? Well, what kind of arguments can you give to
functions? Integers, matrices, polynomials, etc. Yes, that are all
ordinary object or I would rather call them "elements". They are
concrete members of a domain. But what if you write a function that
takes a *type* as input? For example, you know how to construct a
fraction field for any integral domain. Well, then you can write a function
Fraction: IntegralDomain -> Field
as is done in fraction.spad.pamphlet.
https://github.com/hemmecke/fricas-svn/blob/master/src/algebra/fraction.spad.pamphlet#L314
Note that IntegralDomain and Field are of type Category, so there
inhabitants (or values if you like) are what is known as "domains" in
SPAD. A domain is a type.
Using types as arguments in functions means that types are "first class".
You should not be shocked by the fact that the function "Fraction" above
even returns a type and not just an ordinary value (something that I
formerly called "element"). That is what one can do with the type system
of FriCAS.
"List" is another constructor that uses a type as input. (Note, a
"constructor" (in PanAxiom) is a function that returns a type.)
You can, of course easily write functions that take a type as input and
return a value. For example, you want to have a generic list length
function. Then you could write something of the following type.
len: (A: Type) -> (List A -> PositiveInteger)
You would, for example, call this as len(Integer)([3,5,2,7]).
The interesting thing here is there is even a dependent type. The result
type of len is "List(A)->PositiveInteger" and it depends on the value of
the concrete type that you give as the first argument of len.
Yes, you can write
integerListLen := len(Integer)
and then say
integerListLen([2,3,4,8])
Types are "first class", because you can give types as input to
functions. And "dependent types" are types that depend on the input.
Hope that makes it a bit clearer to you. (And I hope other people will
correct me if they think that I've written nonsense.)
Ralf
--
You received this message because you are subscribed to the Google Groups "FriCAS -
computer algebra system" group.
To post to this group, send email to [email protected].
To unsubscribe from this group, send email to
[email protected].
For more options, visit this group at
http://groups.google.com/group/fricas-devel?hl=en.
