Discuss: PLs are characterised by which (iso)morphisms are implemented
- by Yttrill
I am interested to hear discussion of the proposition summarised in the title.
As we know programming language constructions admit a vast number of isomorphisms. In some languages in some places in the translation process some of these isomorphisms are implemented, whilst others require code to be written to implement them.
For example, in my language Felix, the isomorphism between a type T and a tuple of one element of type T is implemented, meaning the two types are indistinguishable (identical). Similarly, a tuple of N values of the same type is not merely isomorphic to an array, it is an array: the isomorphism is implemented by the compiler.
Many other isomorphisms are not implemented for example there is an isomorphism expressed by the following client code:
match v with | ((?x,?y),?z = x,(y,z) // Felix
match v with | (x,y), - x,(y,z) (* Ocaml *)
As another example, a type constructor C of int in Felix may be used directly as a function, whilst in Ocaml you must write a wrapper:
let c x = C x
Another isomorphism Felix implements is the elimination of unit values, including those in tuples: Felix can do this because (most) polymorphic values are monomorphised which can be done because it is a whole program analyser, Ocaml, for example, cannot do this easily because it supports separate compilation. For the same reason Felix performs type-class dispatch at compile time whilst Haskell passes around dictionaries.
There are some quite surprising issues here. For example an array is just a tuple, and tuples can be indexed at run time using a match and returning a value of a corresponding sum type. Indeed, to be correct the index used is in fact a case of unit sum with N summands, rather than an integer. Yet, in a real implementation, if the tuple is an array the index is replaced by an integer with a range check, and the result type is replaced by the common argument type of all the constructors: two isomorphisms are involved here, but they're implemented partly in the compiler translation and partly at run time.
