Idris and ATS

[Andy]

New to Idris. I was looking at ATS recently, which is also a language with dependent type. I wondered how do the type systems of Idris and ATS compare to each other?

Also what kind of performance can I expect from Idris, especially when compared to Haskell and ATS?

Thanks.

[William ML Leslie]

Some of the most significant differences include:

* Idris does not have a syntactic phase distinction.

In ATS, you can see clearly which arguments and values are required at
runtime, and which only exist for the sake of the type, because
irrelevant functions are declared with 'prfun', irrelevant types are
declared with dataprop or dataviewprop etc. In Idris, there are just
functions and datatypes, although functions used in types/proofs need
to be total. The Idris compiler performs a global usage analysis to
determine the things that need to be kept around for the program to
execute. You can declare that you expect certain arguments to be
irrelevant, and the compiler can tell you when that turns out not to
be true.

https://github.com/idris-lang/Idris-dev/wiki/Erasure-by-usage-analysis

* Idris does not have linear types or unboxed types.

Instead, the emphasis is on using embedded DSLs to ensure resources
are reclaimed. (I don't think these are equivalent, but I haven't
come up with a counter-example.) Oh, and there are no seperate types
for closures (as opposed to C-style procedures) in Idris.

* Idris is purely functional.

The real magic of ATS is the fact that, semantically, it's C; so it
lets you prove things about your imperitive programs! Idris has a
package for using and implementing simple algebraic effects, and it's
applicative (not-lazy) by default, so it's not /so/ functionally
opinionated, but I find this to be the biggest draw point for ATS.

* Idris is much cleaner syntactically.

I don't think I need to say much here. Idris looks like Haskell, it's
clear that a lot of thought went into it having a sensible and
consistent syntax.

* Typeclasses and templates.

Idris has a typeclass system. My current understanding of it suggests
that it's slightly more flexible than that of Haskell, because classes
only need to be consistent on any lexical context that tries to infer
them. ATS instead supports function templates, which are something
like C++ templates.

* Performance?

ATS runs /fast/. IIUC there is still plenty of low hanging fruit in
the Idris compiler, but there's really no comparison yet.

The other thing is that I found learning ATS difficult. After reading
the tutorial for a language named Agda, and watching Edwin's video
lectures on Idris, ATS made much more sense to me. I really prefer to
write Idris, I think, although there are still some places I'd rather
use ATS.

--
William Leslie

Notice:
Likely much of this email is, by the nature of copyright, covered
under copyright law. You absolutely MAY reproduce any part of it in
accordance with the copyright law of the nation you are reading this
in. Any attempt to DENY YOU THOSE RIGHTS would be illegal without
prior contractual agreement.

[Andy]

Thanks for the detailed response.

> I really prefer to write Idris, I think, although there are still some places I'd rather use ATS. 

Can you talk about why you prefer Idris and what are the cases where you think ATS is more suited?

[William ML Leslie]

On 25 July 2014 17:15, Andy <selfor...@gmail.com> wrote:
> Thanks for the detailed response.

No worries.

>> I really prefer to write Idris, I think, although there are still some
>> places I'd rather use ATS.
>
> Can you talk about why you prefer Idris and what are the cases where you
> think ATS is more suited?

Idris feels simpler conceptually, it is very easy to get started
writing your idris program. There aren't lots of dark corners of the
language that the tutorial doesn't mention.

ATS is really good at very low level stuff, where you have some
expectation about how your code will look once it is compiled, you can
clearly show that your low-level imperitive implementation matches
your functional spec. If you wanted to, say, implement a garbage
collector or a language runtime, ATS is not a bad choice.

[Brian McKenna]

Here's an example of something I wrote using ATS but couldn't using Idris:

https://github.com/puffnfresh/atsboot

ATS has no runtime which means it can be easier to write embedded
systems or operating systems. If you wanted to do the same for Idris,
you'd have to reimplement the runtime. Maybe ATS is a suitable tool
for implementing that runtime :)

> --
> You received this message because you are subscribed to the Google Groups
> "Idris Programming Language" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to idris-lang+...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.