On 5 September 2010 01:48, Ben Karel <[email protected]> wrote:
> I've only read a few hundred lines of ATS code, and written none, so my
> opinion is worth horsefeathers, but the impression I got was that a rough
> predictor of unreadability is the square of the number of type system
> features used beyond basic ML. The example code for a function that provably
> sorts its input list is cool in theory but (at least to my untrained eyes)
> impenetrable in practice.
It's certainly *Different*. I tried to learn ATS before Agda, but it
wasn't until I learned Agda (which has far, far better tutorials) that
I understood the syntax. The {} all over the place, for example, are
implicit argument lists, inferred by the sorts of other arguments.
I haven't attempted to do anything useful with it yet either, but I'm
itching to. I suspect that the density of the proof functions in
particular want you to write in a literate style.
On 5 September 2010 07:56, wren ng thornton <[email protected]> wrote:
> (code impenetrability) is one of the reasons dependent types haven't moved
> beyond theorem proving and started making a real impact on programming yet.
Or at least that it doesn't provide enough value in return for
programming in-the-large. If you aren't interested in proving
anything, you don't have to do all that work in ATS; the dependent
types are optional.
I think they are valuable in only a handful of places. At the daily
grind for example, information systems tend to be nearly impenetrable
full-stop. In many cases, it's not even clear the original architect
knew what they were doing. If the body of code already present
obscures their original intentions, how much more will additional
type-related noise do so?
But in the off hours I hack on language runtimes and compilers and
hopefully one day, Coyotos. Things both small enough and important
enough to verify aspects of their operation. It's these sort of
systems we are talking about - I can think of several more appropriate
languages for information systems and web applications.
While it is true that few runtimes and compilers are developed in
dependently typed languages, this is probably an artifact of history
more than anything else. In fact, of the popular runtimes and
compilers today, most seem either to be developed when C and C++ were
the language of choice for portability reasons, or were written
specifically for (both on and targeting) the Java or CLI ecosystems.
Of the elephant in the room, the BitC reference compiler, I guess C++
was just what shap and swaroop were most familliar with. I had heard
that it begun its life in python, but little more about that besides
their inability to make it scale.
--
William Leslie
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
