On 21/07/2012, at 8:50 PM, Jacques Carette wrote: > Basically even though T and T^1 are canonically isomorphic,
be good to be able to measure what "canonically" means .. > it is still > not a good idea to remove the 'dimension' component of T^1 entirely, as > you lose uniformity of behaviour of arrays then. > > [You have discovered a number of these things yourself, as I see from > your emails, I am just giving you what I know from experience] Yes. Unfortunately in any programming language, we have a situation where there are three kinds of isomorphism: (a) ones that are identities (b) ones that are represented by identities or casts (c) all the other ones Many functional programming languages use a representation isomorphism that T and pointer to T are isomorphic due to immutability, and this ends up being an "identity" in the type system. In Ocaml for example (ignoring the special case on integers) this is what allows type erasure, intensional polymorphism including run time equality, simple garbage collection, and whole host of other "features" .. essentially its a fraud though. Class b isomorphisms require explicit coercions between two interpretations of the same representation. These are real operations in the type system but no-ops at run time. Felix uses a lot of these "tricks" to model C, for example the option type lines up with C's pointer to object or NULL to allow a raw C pointer to be considered as a sum type without any run time conversion. Every programming language MUST use some fudges, that is, isomorphisms which are regarded as identities. It seems the programming language is actually characterised by such choices. In Felix, compact linear types are proving a pain. Originally these are just a pair of integer values which are mod N and mod M packed into a single integer with multiplication (and extracted with division and modulo). This allows iterating fast through a matrix independently of rank (extending pair to arbitrary tuple). Of course .. now suddenly the "canonical pointer" which I worked so hard to allow Felix pointers and C pointers to be the same (machine addresses) suddenly don't work for the components of a compact linear type .. I need "fat pointers" .. which breaks the current representation invariant. The problem is that the "compact linear types" are pretty much the only way to get polyadic arrays. It can be fixed by making the isomorphism explicit instead of implicit. The problem is that this isomorphism is an *identity*: its a representation conversion between a packed and unpacked value. That's a pretty ugly feature to add to a programming language ;( -- john skaller skal...@users.sourceforge.net http://felix-lang.org ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ Felix-language mailing list Felix-language@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/felix-language
