On Sat, 2006-09-02 at 19:58 -0400, Peter Tanski wrote:
> On Sep 2, 2006, at 2:01 PM, skaller wrote:
> At least in Haskell, a tuple has a formal "type" only in the sense
> that it is a data type defined solely in terms of a constructor. For
> example:
>
> data (,,,) a b c = (,,,) a b c
>
> There are, unfortunately, many "tuple" definitions like this, all the
> way up to 62 in GHC.
OUCH! That's a hack, similar to C++ boost's tuple template.
Felix supports tuples with billions of elements!
It is more advanced than Haskell here: we also have
exponentials:
int * int * int
is a the type of a tuple, we can write this in exponential form:
int ^ 3
Note that 3 is a type:
3 == 1 + 1 + 1
where 1 is the usual unit type, and you can apply
the distributive law:
int ^ 3 = int ^ (1 + 1 + 1) = int * int * int
This is not just syntactic sugar, there is an actual combinator
for it. The type
int * int * int
uses the exponential, always. Such a type is called an array.
In Felix arrays ARE tuples. No, they're not just isomorphic,
they literally ARE tuples.
The specialised representation
t ^ n
can support any n you like (the limit is actually min of
Ocaml 'int' capacity and C++ size_t capacity).
This is a generalised categorical delta function:
delta:: t -> t * t
delta x = x,x
[Cak .. using Haskell notation now .. :]
> Note also that the "name" of this data type is the constructor
> itself. According to the Haskell98 standard the definition of a
> tuple is a "value," not a singular "type,"
Of course: but in Felix, the type is a product type,
that is, a tuple type (which is not the same as a tuple
of types!)
> --------------
> Prelude> let a = (,,) 1 2 3
> Prelude> a
> (1,2,3)
> Prelude> let b = (,,,) 1 2 3
> Prelude> :type b
> b :: forall d. d -> (Integer, Integer, Integer, d)
> --------------
> As you can see from the type of "b" above, there was no syntax error
> and there was also a very odd response: there is an undefined
> existential "d"
why in the heck is this called an existential .. when it
is universally quantified??
> I hope all these examples weren't pedantic. Maybe you already have
> the correct concept named in your head as you read this, but at least
> you understand why the unified TYPE resulting from pair : TYPE * TYPE
> -> TYPE is unusual.
LOL. It isn't unusual in ML or category theory: it is Haskell
that is unusual in trying to use a data type constructor
with arguments in curry form (multiple arguments) to
represent tuples. Theoreticians use this hack too.
> That's exactly what template meta-programming does: it gives the
> programmer special access to values the compiler sees. Meta-
> programming may not be necessary:
Metaprogramming is necessary, but not the way C++ templates
do it ;(
> I am not sure it can't be done
> using Felix's axioms and reductions.
Felix axioms do nothing, except support a runtime
check operation.
Reductions, however, are actually applied
by the compiler.
> > Unfortunately, the Felix type system
> > supports type functions and products:
> >
> > c | -> | *
> >
> > but not sums, so I don't have many constructors to play
> > with other than constants like 'int' :)
>
> You mean, Felix does not have the "disjoint union" type "+"? Tuples
> should properly be disjoint unions. Now there's something to work on.
No, I don't mean Felix doesn't have a sum: contrarily it has TWO
distinct sums: the traditional variants:
union Bool = True | False;
which are nominally typed, and also a structurally typed sum:
int + long
like category theory. The constructor names are canonical:
case 0 of (int + long)
case 1 of (int + long)
which are the first and second injections:
int -> int + long
long -> int + long
respectively. But these are types. What Felix does not
have is sums OF types (as opposed to sum types).
It has tuples of types:
(int, long)
is a pair of types, but there are no sums in the kinding system --yet :)
BTW: tuples aren't disjoint unions. The type of the elements
is a union though:
prj1 : int * long -> int
prj2 : int * long -> long
are the usual projections. However you can then not have a
variable 'projection' because they have distinct types.
This can be fixed:
prj1 : int * long -> int + long
prj2 : int * long -> int + long
so that the projection 'carries' the case index along
with it.
Once you have this formulation, the projections can
be indexed by a *run time* expression, since all
have the same type.
in particular .. for an array, this is the only way
to get array indexing. Actually, you then apply
the 'undelta' function to drop the case index.
--
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net
-------------------------------------------------------------------------
Using Tomcat but need to do more? Need to support web services, security?
Get stuff done quickly with pre-integrated technology to make your job easier
Download IBM WebSphere Application Server v.1.0.1 based on Apache Geronimo
http://sel.as-us.falkag.net/sel?cmd=lnk&kid=120709&bid=263057&dat=121642
_______________________________________________
Felix-language mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/felix-language
