On 16/12/2012, at 3:01 PM, Shayne Fletcher wrote:
> On 15/12/2012 22:59, john skaller wrote:
>> To make matters worse, with compact linear types there are two ways to
>> do indexing:
> That's a key point. I think the trend is towards (and my preference too,)
> that there be one and only one "right" way of doing things.
> Unlike Perl, we seek less ways to skin cats.
This is impossible in any statically typed language (and probably
dynamically typed ones too).
Type systems are rife with morphisms, and isomorphisms always
provide multiple ways to do things (by definition!).
There's always multiple ways to perform some calculation
and multiple choices of data structure.
Worse, sugar adds more ways: the sugared way and the raw way.
Now in this case, we allow
(1,2,3) . 1
(1,2,3) . 1uz
(1,2,3) . (case 1 of 3)
i.e. there's more than one kind of index allowed. Originally it was only type
size but then you had
to write the second style everywhere. The actual virtual function
unsafe_get (a, i)
requires i to be type size.
In the case of Felix f-array (fixed length array) it is a categorical data
structure
which provides
(1,2,3) . (case 1 of 3)
now (it didn't before but it does now!). That's the only option for native
indexing.
However the library array model is designed for dynamic length arrays,
and it has a lot of nice routines (sorting, folds, maps etc) which we want to
reuse for farrays.
Conversely the notation
T ^ N
does not require N to be unitsum anymore. Now, it can be any compact linear
type.
And there's an argument to allow
T ^ string
because JudySL arrays can implement that. We already have the library code
strdict[T]
is precisely an array of T indexed by a string.
Want to get an even worse dl-iemna?
If you could index tuples by a variable this would be the get function
(roughly):
T1 * T2 * T3 ... TN -> N -> T1 + T2 + T3 .. TN
Do you get that? Normally
(1, "Hello", 3.2) . 1 ---> "hello" --> type string
But this is wrong. If that 1 were a variable the result type would
HAVE to be the sum type dual of the tuple type:
(1, "Hello", 3.2) . (case 1 of 3) ---> (case 1 of (int+string+double))
("Hello") -->
type int + string + double
But remember AN ARRAY IS JUST A TUPLE with all elements the same type.
So we cannot justify even the primitive array indexing: its just plain wrong.
the correct array indexing function is exactly the same as the tuple case:
(1,2,3) . (case 1 of 3) -> (case 1 of int^3) (2) --> type int * 3
Note the type int * 3 assuming that equals int + int + int (which isn't
implement yet in Felix!!! Note also RUST got this notation completely
wrong following LLVM. Someone didn't do their theory homework!)
It's very important to note that the CORRECT result from the array
carries the index with it, as well as the value. This is really useful!
The RIGHT WAY to fix the return type for tuples is to do a match.
But for arrays, there's no need. There's a categorical function
that "throws away the index":
smash : int * 3 -> int
[Written as an upside-down delta, since delta is the inverse
function, namely the diagonal function T -> T^N which
makes N copies of a value]
So actually we should have to write:
smash ( a . i )
for arrays (this would be a compile time error for non-array tuples:
smash requires an argument of type T * N)
So now, if I fully did this right, array indexing got even more complicated!
Remember some things are isomorphic but not equal, for example:
2 * 2 === 4 but 2 * 2 != 4: isomorophic but not equal
Similarly tuple and sum formation isn't associative but every permutation
and nesting of them is isomorphic to every other.
What characterises a programming language is what isomorphisms are
considered equalities, and, which representation isomorphisms are
reinterpret casts so that conversions have zero cost.
Felix has some pretty clever representations. And some really MESSY ones
designed for performance at the cost of restrictions and complexity,
eg compact linear types: slower, mess up pointers, have size limits,
but allow maximally compact storage of data (guaranteed!), and,
support polyadic arrays (a nice bonus which is the real reason
to have them :)
Every language makes compromises. For example Haskell's type
classes are plain wrong. They assume a canonical set of functions
for a type. Which means you only get ONE model of the type.
So for example integers are totally ordered, in ascending order
but not descending order (even though that too is a total order).
Ocaml's module system is more general. But you have to explicitly
supply a module argument to a functor before you can use
any of the "virtual functions". Worse, you have to create binding,
and you can only do that in limited contexts, not "anonymously inline".
Haskell and C++ and Felix allow the anonymously inline advantage
at the cost of being limited to a canonical model.
This may sound like a minor issue but it is really biting me on the butt
with respect to arrays.
--
john skaller
skal...@users.sourceforge.net
http://felix-lang.org
------------------------------------------------------------------------------
LogMeIn Rescue: Anywhere, Anytime Remote support for IT. Free Trial
Remotely access PCs and mobile devices and provide instant support
Improve your efficiency, and focus on delivering more value-add services
Discover what IT Professionals Know. Rescue delivers
http://p.sf.net/sfu/logmein_12329d2d
_______________________________________________
Felix-language mailing list
Felix-language@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/felix-language
