On 25/12/2012, at 7:10 PM, Raoul Duke wrote:
> 2nd'd (although i'm just a language "groupie", not a 'trusted
> authority' on such things :-)
There are no authorities (though Oleg comes dang close :)
>
> note that iirc from the ats list, one wants to be looking at / using
> ats2, since ats is deprecated pretty much.
Er .. any references?
> please also note the part
> of the ddc dissertation that says the dependent etc. typing notation
> in ats quickly becomes entirely too unwieldy. :-(
I haven't got up to that yet in my reading.
However theoretically nice stuff often goes that way.
Another example is open recursion. In Ocaml with polymorphic
variants you can do open recursion, Felix used to do this for
the type terms.
Basically instead of a recursive type
type t = ... Ctor of t ...
you write
type 'a t = ... Ctor of 'a ...
so you have a non-recursive type with a parameter. You can make this
open type closed by recursion:
type ct = 'b t as 'b
however since the type is extensible you can also extend it and THEN
close the extension:
type 'a t2 = [ 'a t | Ctor2 of 'a ...]
type ct2 = 'b t2 as 'b
These two types are related: ct is a covariant subtype of ct2.
This was used in Felix like:
real types = ....
super types = real types + lambda-abstractions + applications + pattern
matches ..
the idea being that a real type is formed by reduction of a super type. This
makes
it possible to annotate algorithms with the more precise type it handles,
instead
of having to "assert false" on the types that aren't supposed to turn up at that
point.
The problem is .. types, expressions, patterns, constraints .. etc there are
about 14 sorts of term.
So whilst open recursion works fine with 1 parameter, it gets a bit tricker
with 2,
it is almost impossible to manage with 3, and with 14 you need a super computer
to write out all the combinations. Assert false is just easier :)
ATS is all about precision. And the above is why precision doesn't work.
In Felix today there are examples, for example the type of functions
and generators is the same. I could easily make them distinct.
Say:
f: A -> B // function
f: A >-> B // generator
But then if you have a higher order function like
fold: (A -> B -> B) -> B -> list[A]
it wouldn't work with generators so you'd need another variant that does,
and it would all be very confusing!
This is also why I threw out "const". It adds precision, but the complexity
is not worth it.
ATS is interesting because it makes type distinctions which reflect the
representations of types at a lower level than Felix, for example
it has boxed and unboxed types. Felix has pointers, but it isn't
the same. Felix has no intensionally polymorphic functions,
but there is a (currently disabled due to bug) algorithm that optimises
away copies of duplicate instantiations which differ only in
pointer types (i.e. T* is converted to void* and we do casting
precisely how you'd do polymorphism in C).
That is, Felix tries to keep these things out of the type system.
For example you probably think:
fun f: int -> int = "$1+1";
is a Felix function. It isn't. Its a macro. But you can use it as a function!
var ff = f;
...
Oh yes that works, because Felix secretly generates a wrapper which
is a function :) It does this for union constructors too, and for C functions.
Glossing over categorical distinctions isn't always good.
It really complicates things in the compiler and leads to surprises
when the rules turn out to be unsound.
In fact the on that has my nickers in a knot at the moment is
the compact linear type .. it's a special representation for
types like:
3 * 2 * 5
in a single int (very much the same idea as C bitfields only
even more compact).
Felix tries to hide the representation change from
addressable fields. It would be much easier for me if
there were a distinct type and a pair of conversions the
use had to write explicitly.
This is the key issue for PL design really. Which isomorphisms
are silently hidden by the compiler? Which require user invocation?
Which correspond with sweet syntax? Which map to representation
compatibility?
--
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
