Idris 1.5: the best tool for _____?

[Dean Thompson]

It is wonderful to have Idris 1.0 on the street. Idris is already fantastic for exploring programming with dependent types. But personally, I like Idris so much that I want to help it go mainstream.

For Idris to go mainstream, I propose we need to do the following:

- We need to decide that a near-future version of Idris will be a great tool for some particular kind of programming in some particular domain. (I say 1.5 above to be provocative.)

- To do that, I think we almost certainly need to coopt some existing ecosystem. We need an excellent runtime environment and a big set of libraries that we don't have the manpower to build from scratch.

Given where we stand right now, technically, the obvious ecosystem to coopt would be JavaScript: Node.js and/or browser. But I lean strongly against this as a primary choice. JavaScript is focused on a problem -- developing web applications -- that, while still important, is old and well-solved. I don't think Idris can meaningfully displace technologies like Node and React in that space. Also, I think the culture and typical preferences of the web application world are diametrically opposed to a fancy static type system.

The following huge developer survey from Stack Overflow may be a useful shared point of reference: http://stackoverflow.com/insights/survey/2016 . If we want to see people using Idris to solve real-world problems, which of the people in this survey might we realistically try to attract? I don't think we necessarily want to aim at a large slice. We might be better off aiming at a small but meaningful slice -- especially if it is a growing slice.

I already mentioned that I feel web applications already have dominant stacks, tools, and tastes, and predict those developers won't move. I feel the same way about data science and machine learning. 

Both mobile and desktop UI development are strongly pulled into the orbits of their vendors (mainly Apple and Microsoft) -- I spent a while digging into the state of the art of cross-platform UI development, and concluded it is dismal. So I don't think that's it, either.

Personally, I lean toward focusing on the domains other than AI that I believe will be most important in the coming 20 years: augmented reality, virtual reality, gestural interfaces, robotics, ubiquitous sensors, and Internet of Things. If we aim Idris at problem domains that are very small slices now, but that will grow, we may be able to focus tightly on making Idris a great tool now in a narrow space and then grow with it.

C++ has by far the most momentum in those problem domains. My leaning is that a certain set of programmers who are technically strong and who care more about the problem domain than about the language or programming experience will continue to use C++. I think it will be difficult to entice C++ programmers to Idris. I also think the huge impedence mismatch between C++ and every other language makes it very difficult to coopt the C++ ecosystem.

I think JavaScript is next behind C++ in those problem domains. Python is probably next behind JavaScript. I believe JavaScript and Python will continue to gain momentum in these problem domains, but mostly by programmers who already know those languages and/or are drawn by their approachability and momentum. Those technology stacks are not well suited to the problem domain. I can't picture Idris attracting those programmers. Certainly those stacks are not good platforms for Idris to attack those problem domains.

Go has recently picked up interesting momentum in those problem domains. As I write this, I am personally leaning toward Go as a platform and adopted ecosystem for Idris. It isn't that I want to program in Go -- I really don't! -- but:

- I think there's a fighting chance that we could automate a non-terrible Idris wrapper for Go APIs. (I'm pretty certain this is infeasible for C++ -- that impedance mismatch just seems huge to me.)

- I am interested in a Go backend for the Idris compiler, as a way of targeting a fast runtime system. From this perspective, I like the fact that the Go compiler is very fast.

- Although the Go ecosystem is much smaller than the C++ ecosystem, I suspect the total amount of Go open source created in the past couple of years is higher than the total amount of C++ open source created. That may be more important.

Another candidate for ecosystem to coopt would be Rust. I am personally very fond of Rust -- not from having written much code in it, but from having followed its development fairly closely and having read Rust code. But Rust has negligible momentum compared to Go, and may yet fail. Also, it is much more complex than Go, so surely more difficult to API-wrap. Plus, it has a very slow compiler, so a Rust backend for Idris wouldn't work well. Instead, we'd use an LLVM backend, which I find very attractive, but which feels much harder to me than a Go backend. All that said, it is very interesting to me that Rust tops the "Most Loved" language list in the survey I referenced above. Rust asks for a lot of up-front intellectual energy from the programmer. It yields rigorous, safe, fast code in return. These characteristics are akin to Idris. Although Rust has some wonderful abstraction support, I think the demand it places on careful thought about use of memory makes it in many ways a low-level, close-to-the-metal language. Is there room for a very high-level language like Idris to join the Rust ecosystem in some way?

Thoughts?

Dean

[Gregg Reynolds]

On Apr 13, 2017 9:35 AM, "Dean Thompson" <deansher...@gmail.com> wrote:

It is wonderful to have Idris 1.0 on the street. Idris is already fantastic for exploring programming with dependent types. But personally, I like Idris so much that I want to help it go mainstream.

For Idris to go mainstream, I propose we need to do the following:

- We need to decide that a near-future version of Idris will be a great tool for some particular kind of programming in some particular domain. (I say 1.5 above to be provocative.)

- To do that, I think we almost certainly need to coopt some existing ecosystem. We need an excellent runtime environment and a big set of libraries that we don't have the manpower to build from scratch.

...

Thoughts?

not sure what you mean by coopt, but the jvm is quite popular as a host env for a variety of popular languages (clojure, scala, kotlin, etc.)  a quick web search show several idris-java projects.  i haven't used any of them, would be interested in status reports.

gregg

[john NeuMotiveLLC]

SPARK, Ada, Notepad++, Atom b/c formal methods, probability, verification, types

[john NeuMotiveLLC]

SPARK, Ada, Notepad++, Atom b/c formal methods, provability, verification, types

[Gregg Reynolds]

On Apr 13, 2017 1:16 PM, "john NeuMotiveLLC" <neum...@gmail.com> wrote:

SPARK, Ada, Notepad++, Atom b/c formal methods, provability, verification, types

On Thursday, April 13, 2017 at 12:07:19 PM UTC-6, john NeuMotiveLLC wrote:

SPARK, Ada, Notepad++, Atom b/c formal methods, probability, verification, types

great list. what does it mean?

[neum...@gmail.com]

Sorry, reply should have been to Dean looking for compatible user base to leverage toward Idris.

--
You received this message because you are subscribed to a topic in the Google Groups "Idris Programming Language" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/idris-lang/xX5rUI1kKMM/unsubscribe.
To unsubscribe from this group and all its topics, send an email to idris-lang+...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

 

[Pierre Beaucamp]

Hi,

I share the sentiment of wanting to help Idris go mainstream. But I want to add a bit of background what makes me believe in Idris and why I feel that concentrating on a particular domain to adopt is a bad choice in my opinion.

Before I discovered Idris, I was mainly a Go developer. I still use and advocate for Go at my workplace and would consider myself an active participant in the Go community.
Go was never designed for a specific domain. Go was designed to by a strongly opinionated, modern, and simple language. I don't know of any Go developer who wouldn't agree that C might be better suited for low level development, Rust for stronger safety guarantees or Python for just quickly creating a script. The reason for the success and huge adoption of Go is that it comes with sane defaults, is highly adaptable to any domain and that the language makes it genuinely hard to shoot yourself in the foot. A lot of people don't like Go for exactly those reasons and feel like the language restricts them too much, yet it's next to unprecedented in development speed for a proper AOT compiled language.

Incidentally, I was very interested in Haskell and functional languages in general. But Haskell feels just too complex - it's the polar opposite of being opinionated. The learning curve for Haskell is already steep enough for someone who never had to deal with side-effects before, but now every blog post, tutorial or successful Haskell project uses their own flavor of Haskell. (I'm talking about stuff like language pragmas and countless libraries to achieve essentially the same thing using a slightly different way).

I was initially a big fan of PureScript, but since I discovered Idris I'm considering it my go to language. The reasons I like Idris are:

• It's general purpose
• The language itself is simple, but empowers you to do complex things
• It's (at least right now) relatively uncluttered in terms of ecosystems and tools, making it easy to pick up
• It features different backends - I can compile to JS to execute in the browser but I can choose a different one for server side execution.
  

I specifically hope that Idris won't be know for the "best language to do x". I hope it stays general purpose and people will pick it up to have a strongly typed language with sane defaults, which they can't find anywhere else. Over time, a natural fit for a specific domain will emerge. At least, that's what I wish for this language.

Best Regards,
Pierre Beaucamp

[Michael Litchard]

I think idris will shine as a way to create a DSL. Imagine writing a DSL that looks alot like, say python, but could not blow up in the familiar ways python can blow up. That way, you have a pool of engineers who can be productive in the python-esque DSL. And they don't have to know idris. Only the person who wrote the DSL does.

--
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+unsubscribe@googlegroups.com.

[Tim Steenvoorden]

Hi Dean,

A Go backend for Idris would of course be nice to have. Especially when calls to Go functions are available. Writing a Go backend wouldn’t be very difficult and could probably be done in a day or two. Implementing a proper foreign function interface is a bit more work, as well as optimising for tail calls. You’ll probably need trampolines or the like, I don’t know how the JavaScript backend handles this at the moment.

I’d be more interested however in an optimised backend and runtime for Idris which properly uses uniqueness and/or the information from linear types. Exploiting uniqueness to assure program’s will use less than a certain amount of memory or no heap at all would be amazing. Imaging the gains for embedded systems and the like!

Cheers,

Tim

----

T.J. Steenvoorden, MSc

PhD Candidate | Radboud University Nijmegen

Faculty of Science | Department of Software Science

Mercator 1 Building | Room 01.08

Toernooiveld 212 | 6525 EC | Nijmegen | The Netherlands

+31 24 365 22 91 | t.steen...@cs.ru.nl

To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.

[Cliff L. Biffle]

On Tue, Apr 18, 2017 at 7:13 AM, Tim Steenvoorden <tim.stee...@gmail.com> wrote:

I’d be more interested however in an optimised backend and runtime for Idris which properly uses uniqueness and/or the information from linear types. Exploiting uniqueness to assure program’s will use less than a certain amount of memory or no heap at all would be amazing. Imaging the gains for embedded systems and the like!

FWIW, I'm not sure you can do this in Go, but this would be useful (and probably required) for a Rust backend. :-)

I'd want to see it work in a C backend first, of course.

-Cliff

[Tim Steenvoorden]

Hi Cliff,

It certainly isn't possible in Go! I was referring to a separate backend with those features ;-)

Cheers,
Tim

----

T.J. Steenvoorden, MSc

PhD Candidate | Radboud University Nijmegen

Faculty of Science | Department of Software Science

Mercator 1 Building | Room 01.08

Toernooiveld 212 | 6525 EC | Nijmegen | The Netherlands

+31 24 365 22 91 | t.steen...@cs.ru.nl

--

[Kris Nuttycombe]

Something that I would love to see, and that I think essentially demands a dependently-typed, purely-functional, total language, is a typed data frame library providing functionality that is akin to what is available in Python's "pandas" library, or the R and Julia languages. At present, there is essentially no language that I know of that provides this kind of functionality along with the ease of maintenance and error-checking that typed languages provide. 

Buzzword or not, "data science" is increasingly important in industry, but the process of putting code written in any of the major "data science languages" into production is arduous, not least because the standard way of dealing with errors or incompatible values is to throw seemingly unrelated exceptions from deep in the guts of libraries distant from the source of the bad data. I suspect that a language like Idris, with sufficient effort, has perhaps the best chance of making computing on multidimensional data like this rigorous and safe, and ultimately significantly more performant than anything that dynamic languages can offer.

Kris

--
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+unsubscribe@googlegroups.com.

[Bryn Keller]

This. A replacement for Python/R/Matlab, with strong support for distributed/parallel computing a la Spark or MPI, with outstanding typing, and where I can, if I like, *prove* my results. A lot of effort would be required, to be sure, but this would be a fantastic goal.

[Gregg Reynolds]

On Apr 19, 2017 10:23 AM, "Kris Nuttycombe" <kris.nu...@gmail.com> wrote:

Something that I would love to see, and that I think essentially demands a dependently-typed, purely-functional, total language, is a typed data frame library providing functionality that is akin to what is available in Python's "pandas" library, or the R and Julia languages.

+1

[Dean Thompson]

To me, it seems as though Python has an unassailable hold on data science. The Python data science ecosystem is immense and has huge momentum. Astoundingly, it seems poised to eclipse R and Matlab, which each have huge, older ecosystems and great momentum. It is hard for me to imagine Idris becoming the best tool for even a small slice of the data science audience.

Also, I worry that most data science programmers wouldn't want to invest in learning how to use a fancy type system. I doubt they are our programmer audience. 

I lean against a frontal attack on a well-served problem domain. I feel as though we need to choose a poorly served problem domain and serve it well. 

Dean

--

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.

[bo...@pik-potsdam.de]

Dean Thompson <deansher...@gmail.com> wrote:

> ...

>
> I lean against a frontal attack on a well-served problem domain. I
> feel as though we need to choose a poorly served problem domain and
> serve it well. 

What about starting a frontal attack on programming in Idris?

The language seems to be an ideal tool for expressing what programs are
meant to do.

But, perhaps paradoxically, many if not most of the basic programs, say,
from the Idris prelude, lack precise specifications.

How can we credibly propose a methodology for verified programming that
relies on unspecified (let apart unchecked) components? Why not starting
by doing our own laundry?

A systematic attempt at specifying that 'filter' shall filter, 'nub'
shall nub, 'delete' shall delete, etc. looks at the first glance like a
modest, boring exercise. It is not!

The exercise would provide useful insights on the current state of the
language. And a specification of the most basic Idris components would
provide a minimal proof of concepts for language constructs and
programming idioms which are meant to support program verification.

In short, it seems to me that a measured attack on Idris would be a
modest but necessary first step before taking up the challenge of
eradicating the evil from well-served, specific domains.

Another obvious advantage of such an attack is that none apart from
ourselves could blame us for the move.

Best,
Nicola

[Kris Nuttycombe]

The principle reason I suggested the data science problem is that I'm currently responsible for maintaining a python/pandas codebase, and it'd be hard to describe it as anything other than a complete nightmare. The standard failure mode is throwing exceptions, nothing documents what exceptions it may throw, and even doing something as attempting to perform an operation on an empty data frame is likely to crash your program. There's a distinction between data science being done in an exploratory capacity, which is as you say relatively well-served by python, and "data science" operations being integrated into a production system with more stringent failure tolerance requirements; this latter space seems to me not at all well-served by any of the environments I'm aware of. In fact, one of the more common complaints I hear from organizations is the difficulty they have in "productionizing" the prototypes (usually written in R or python) that were built by their data science teams.

You're right about momentum, for sure, and that it might be just too big of a hill to climb for the Idris community. However, I think that the rewards would also be huge, not merely for the users of such a set of libraries, but for the development of Idris itself; it's not an easy problem, and it would require both figuring out how to express the constraints on the types of such multidimensional data in a comprehensible fashion *and* starting to take a serious look at how to make programs written in Idris performant.

To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+unsubscribe@googlegroups.com.

For more options, visit https://groups.google.com/d/optout.

--

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+unsubscribe@googlegroups.com.

[Anand Patil]

+1 to the data science idea. Trying to take over the world and displace Python/R would be pretty difficult; but I think there is a latent community out there who could coalesce around a sufficiently productive, safer option and would enjoy major benefits. The Idris data science community would always be a minority, so Idris' data science tooling would have to be designed around the need to dip into R and Python from time to time.

However, I wonder whether Idris or Haskell/OCaml is the right home for this effort. Idris clearly is the better foundation for a very safe array / data frame DSL; but Haskell or OCaml could provide huge safety improvements relative to Python and are way ahead of Idris in things like library coverage, tooling, compiler maturity and industry adoption.

On Thu, Apr 20, 2017 at 10:33 AM Kris Nuttycombe <kris.nu...@gmail.com> wrote:

The principle reason I suggested the data science problem is that I'm currently responsible for maintaining a python/pandas codebase, and it'd be hard to describe it as anything other than a complete nightmare. The standard failure mode is throwing exceptions, nothing documents what exceptions it may throw, and even doing something as attempting to perform an operation on an empty data frame is likely to crash your program. There's a distinction between data science being done in an exploratory capacity, which is as you say relatively well-served by python, and "data science" operations being integrated into a production system with more stringent failure tolerance requirements; this latter space seems to me not at all well-served by any of the environments I'm aware of. In fact, one of the more common complaints I hear from organizations is the difficulty they have in "productionizing" the prototypes (usually written in R or python) that were built by their data science teams.

You're right about momentum, for sure, and that it might be just too big of a hill to climb for the Idris community. However, I think that the rewards would also be huge, not merely for the users of such a set of libraries, but for the development of Idris itself; it's not an easy problem, and it would require both figuring out how to express the constraints on the types of such multidimensional data in a comprehensible fashion *and* starting to take a serious look at how to make programs written in Idris performant.

On Thu, Apr 20, 2017 at 5:55 AM, Dean Thompson <deansher...@gmail.com> wrote:

To me, it seems as though Python has an unassailable hold on data science. The Python data science ecosystem is immense and has huge momentum. Astoundingly, it seems poised to eclipse R and Matlab, which each have huge, older ecosystems and great momentum. It is hard for me to imagine Idris becoming the best tool for even a small slice of the data science audience.

Also, I worry that most data science programmers wouldn't want to invest in learning how to use a fancy type system. I doubt they are our programmer audience. 

I lean against a frontal attack on a well-served problem domain. I feel as though we need to choose a poorly served problem domain and serve it well. 

Dean

On Wed, Apr 19, 2017 at 2:46 PM Gregg Reynolds <d...@mobileink.com> wrote:

On Apr 19, 2017 10:23 AM, "Kris Nuttycombe" <kris.nu...@gmail.com> wrote:

Something that I would love to see, and that I think essentially demands a dependently-typed, purely-functional, total language, is a typed data frame library providing functionality that is akin to what is available in Python's "pandas" library, or the R and Julia languages.

+1

--
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.

--
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.

--
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.

[Nelson]

A problem with Python is that it is a bit slow (I suppose that Python, with libraries written in C, is fast enough in most use cases), whereas parallel programming languages address the speed issue by making it extremely easy to utilize all the cores of one machine and all the machines within a cluster.  Chapel, open sourced, funded by Cray, actively developed, is an example.  X10 by IBM is another.

http://chapel.cray.com

I saw this video on youtube, and actually we can just fast forward to the last 3 minutes or so when the speaker demonstrated the speed increase of his algorithm using Chapel instead of Python.

https://youtu.be/KuoiYDnrYqU

Concurrency and multi-cores programming is required now for not only supercomputers, but also desktops and laptops sold on main street.   AMD Ryzen provides relatively low cost 8 cores to the public and Intel will respond by releasing 6 cores Coffee Lake and up to 12 cores Skylake-X in just a few months.  New computer games can use 8 cores or more, and data scientists will want an ecosystem encouraging them to effectively use all available cores.  Python, R , Matlab, being single core programming languages, are vulnerable on the thrones of data science.  Idris, with safe dependent types and beautiful Haskell inspired syntax, when placed on a real concurrency runtime (maybe Chapel), may slice a share of data science realm.

[Cody Goodman]

I personally want a typesafe pandas. Something like frames (https://github.com/acowley/Frames) with a simpler implementation thinks to type providers and hopefully custom errors.

Imagine being able to immediate query an sql database whose type is provided to you but with the convenience of doing the same in a pandas reply.

[Joheinz]

For me idris would be the best tool to learn about dependent type systems.

That includes
- first grade error messages
- excellent documentation
- standard library of exceptional quality
- proofs inside the library (what Nicola said)
- proofs for standard category theory constructs (functors,
applicatives, monads, ...)
- a proper way to organise, find and reuse proofs
- an established coding standard
- an easier way to interface with foreign libraries
- a remotely functional packaging system and an infrastructure to
use/download packages
- supported external libraries (aka developers which are commited to
providing working versions as the language develops)
- the courage to develop the language in favour of achieving backwards
compatibility

Markus

2017-04-20 22:57 GMT+02:00 Cody Goodman <codygman....@gmail.com>:
> I personally want a typesafe pandas. Something like frames (https://github.com/acowley/Frames) with a simpler implementation thinks to type providers and hopefully custom errors.
>
> Imagine being able to immediate query an sql database whose type is provided to you but with the convenience of doing the same in a pandas reply.
>

[William ML Leslie]

I feel that data science, and in fact most of python's territory, is not an ideal first direction to step in.  That said, I've maintained ESRI codebases written by people who had clearly never smelled a python tutorial, so I have a small handle on what you're saying Kris.  It would be /nice/ to be able to port that same code to a language like Idris easily.

​I want to first talk about why I think this is not a useful direction, then suggest one that I think might be worthwhile.  I'm really ranty, I know.  I'm sorry.  Writing software mostly sucks.​  Ranting about writing software is a fine salve.

Speed
=====

I'll use Nelson's email as a starting off point:

On 21 April 2017 at 04:47, nelson chen <agen...@gmail.com> wrote:
> A problem with Python is that it is a bit slow (I suppose that Python, with
> libraries written in C, is fast enough in most use cases), whereas parallel
> programming languages address the speed issue by making it extremely easy to
> utilize all the cores of one machine and all the machines within a cluster.
> Chapel, open sourced, funded by Cray, actively developed, is an example.
> X10 by IBM is another.
>
> http://chapel.cray.com
>

For data science, it doesn't matter so much if python or matlab are slow or single-core.  Most of the operations people do are simple operations on large arrays, which means most of the computation can be done on the GPU, or when that isn't present, the vector registers.  This is why libraries like numpy and numexpr have made such a splash.  It doesn't matter that the language is friendly rather than fast; because the hard work is done elsewhere.

At the same time, there's a large class of programs that can't take advantage of blas/lapack or hand off to some shaders (and many that can't efficiently run on the GPU at all).  If the problem is mild, these people write cython.  If the problem is extreme, another

​trend​

 tends to happen.

​..​

For those that care more about execution time and small-scale distribution (8-50 cores) than ease of use, they move to other languages.  To Go, to Elixir, to Rust, to Haskell, to Julia, to D. These people have already moved; it's not easy to get them to switch to anything else.  Anyone in that position will immediately reach for one of these languages, attempting to eclipse any of them is not going to be an easy path.

Side note on X10:  I've used its compiler back-end, FIRM, extensively.  That has so much global state that using it concurrently is effectively impossible.  I'm not sure why people building highly concurrent systems keep doing this to themselves.  It also has the offensive behaviour of aborting when it detects an error.  Still nicer than LLVM, though.  If anyone wants to port FIRM to Idris or Agda that would be so very awesome.

Safety
=====

> On Thursday, April 20, 2017 at 8:17:32 AM UTC-7, Anand Patil wrote:
>>

>> +1 to the data science idea. Trying to take over the world and displace
>> Python/R would be pretty difficult; but I think there is a latent community
>> out there who could coalesce around a sufficiently productive, safer option
>> and would enjoy major benefits. The Idris data science community would
>> always be a minority, so Idris' data science tooling would have to be
>> designed around the need to dip into R and Python from time to time.
>>

There's a C++ library called Armadillo that people seem to like; Idris could

​do something similar and do a much better job of it​

.

http://arma.sourceforge.net/faq.html

>> However, I wonder whether Idris or Haskell/OCaml is the right home for
>> this effort. Idris clearly is the better foundation for a very safe array /
>> data frame DSL; but Haskell or OCaml could provide huge safety improvements
>> relative to Python and are way ahead of Idris in things like library
>> coverage, tooling, compiler maturity and industry adoption.
>>

Another side note: am I the only one who finds the worst thing about Haskell is the tooling?  For a language whose proponents like to claim that it's easy to reason about, doing any offline reasoning on it is a pain in the neck.  Say, you want to find all places a constructor is applied.  What tool do you reach for?  Do you grep for the constructor and then muddle through which lines are applications and which are patterns?  Do you grep for imports?  I just don't know.  Honestly, Idris is miles ahead in terms of tooling (thanks, idris-mode).  It's not quite Agda, but it's good.

Also, tying a lazy language and an eager one together nicely is non-trivial.

>> On Thu, Apr 20, 2017 at 10:33 AM Kris Nuttycombe <kris.nu...@gmail.com>
>> wrote:
>>>
>>>  In fact, one of the
>>> more common complaints I hear from organizations is the difficulty they have
>>> in "productionizing" the prototypes (usually written in R or python) that
>>> were built by their data science teams.
>>>

Have you found that uncaught exceptions are the main problem when productionising a data science pipeline, or does it tend to be ambient access to files and network, as well as people catching exceptions too eagerly or without enough specificity?  I've often found it's these very external effects that tend to cause problems:  scripts copying geospatial databases around and sending emails when they are done, reading flat files off network shares, and the dreaded `except:`.

You could argue that types would make these sort of problems easier to identify and fix; but it just means people create a giant monad stack and give it an innocuous name like Idris.  All the inscrutability of first-class effects, none of the usability.

>>> *and* starting to take a serious look at how to make programs
>>> written in Idris performant.
>>>

+1

>>> On Thu, Apr 20, 2017 at 5:55 AM, Dean Thompson <deansher...@gmail.com>
>>> wrote:
>>>>
>>>> To me, it seems as though Python has an unassailable hold on data
>>>> science. The Python data science ecosystem is immense and has huge momentum.
>>>> 

I'm lucky enough to have both a paid government job doing applied mathematics and have enough free time that I can work on what I want in the evening.  You know what the suckiest thing is about programming for me, day in, day out?  It's that I usually only get to use Python when I'm not working.  So I implore: help me never have to write Java or Ruby again.  Let Idris be the decent language that my snooty CTO finally says "ok" to productionising.  I don't need you to replace my Python,

​

​

​

it's not dead,

​

it's just pining for the fjords

​

(until Monte comes along)

​

.

Oh yeah, what

​*​

would

​*​

​it take to replace Java in my workplace​

?  Hmm.

A Pony and a Plastic Rocket

=======

​====================​

If I was to try to drag my workplace off Java, what would the replacement need to have?  Well, at my office, everyone[0] is into this awful client-side framework called Google Web Toolkit.  What is nice about it?  Nothing that I can tell.  If I had to reach for a strongly-typed language to use on the browser, I'd have gone for Elm.  I guess that we do get to use the same tooling (mostly class generation) on the client as we do for the server, and there are libraries for standard widgets.

Maybe that's the key, full stack with an icky enterprise MVC framework on the client?  Whenever I've spoken to GWT proponents, they seem to talk about being able to support different ES versions as well as the wonders of abstract interpretation for optimising.

What about Ruby?  Well, we mostly use Ruby for its DSLs and templating.  We generate much of our transfer and persistence layers, often for several languages that we need to use.  Idris already has the DSLs down.​

[0] That is, the CTO.  We all moved to it in 2012 as an experiment, and it was slow, impossible to debug, and flaky as anything.  Slowly, most people avoided working in it.  Normally I end up the only person willing to work with whatever awful knee-jerk tech decision the higher-ups had made, but this time I stepped back quickly enough.  Phew.

--
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.

[Alex Babkin]

I think Idris would make a good candidate language for writing formally verified languages/DSLs to express smart contracts.
Blockchain/Smart-contracts (e.g. https://www.ethereum.org/ , https://www.hyperledger.org/) looks to be an up and coming new hot area of R&D but arguably still is lacking a good formally verified language that one could express the contracts in without worrying about forgetting to capture corner cases that could be exploited (https://medium.com/@MyPaoG/explaining-the-dao-exploit-for-beginners-in-solidity-80ee84f0d470)

Ability to express a state-machine with constraints encoded in dependent types and Idris' function totality checks, would be very handy in this particular area.

On Thursday, April 13, 2017 at 10:35:46 AM UTC-4, Dean Thompson wrote:

[Gregg Reynolds]

On Apr 20, 2017 10:17 AM, "Anand Patil" <anand.prab...@gmail.com> wrote:

+1 to the data science idea. Trying to take over the world and displace Python/R would be pretty difficult; but I think there is a latent community out there who could coalesce around a sufficiently productive, safer option and would enjoy major benefits.

lurker here, wondering about starting small.  data cleaning is a huge and very expensive problem in the social sciences. imputation (https://en.m.wikipedia.org/wiki/Imputation_(statistics)) is a big deal.  is Idris iny any way better suited than other languages to tackle such problems?

 gregg

[Michał Kłeczek]

It is worth looking at

https://publications.lib.chalmers.se/records/fulltext/234939/234939.pdf

[bo...@pik-potsdam.de]

I very much agree with Markus's comments. Elaborating on the point that
I was trying to make in my previous post:

My suggestion is to start by re-writing a few Idris basic libraries in
terms of precise specifications. Proofs would also need to be provided,
but only later, after we have agreed on well understood specifications.

For example, elaborating on a related thread on library philosophy, I
suggest replacing the current specification (specification through
implementation is over-specification!) of |length| from the prelude:

length : List a -> Nat
length [] = 0
length (x :: xs) = 1 + length xs

with something like

length : List a -> Nat
lengthSpec0 : length Nil = Z
lengthSpec1 : (x : a) -> (xs : List a) -> length (x :: xs) = S (length xs)

This would pave the way for providing different implementations of
|length| in separated modules.

Users would be able to apply fast, accumulator-based implementations,
canonical implementations, fold-based implementations, parallel
implementations, etc. simply by importing different modules.

Separating implementations from specifications is a necessary first step
for applying Idris to large scale project. The approach currently
adopted in the basic Idris libraries does not scale up very well. If we
try to apply it to large scale projects, it leads to libraries which are
brittle and difficult to maintain. In the above example, for instance,
every minor change in the implementation of |length| would force
rewriting most proofs of properties involving |length|.

For large scale projects, this is not acceptable: if we want to apply
Idris to build libraries for specific application domains, we first have
to show that we have a methodology that support verified programming
without compromising maintainability. Re-implementing a few basic Idris
libraries seems an obvious proof of concepts for such a methodology.

A clearcut separation between specification and implementations seems an
obvious first step towards developing a methodology for providing stable
collections of verified implementations. Thus, for instance, one could
provide a |mapPreservesLength| implementation for lists

mapPreservesLength f Nil = ( length (map f Nil) )
={ Refl }=
( length Nil )
={ lengthSpec0 }=
( Z )
={ sym lengthSpec0 }=
( length Nil )
QED
mapPreservesLength f (x :: xs) = ( length (map f (x :: xs)) )
={ Refl }=
( length (f x :: map f xs) )
={ lengthSpec1 (f x) (map f xs) }=
( S (length (map f xs)) )
={ cong (mapPreservesLength f xs) }=
( S (length xs) )
={ sym (lengthSpec1 x xs) }=
( length (x :: xs) )
QED

that hold for any implementation of |length| as far as this fulfills the
specification.

Separating specifications and implementations also seems a critical step
towards promoting the specification-driven (type-driven) software
development approach we believe in. Applying such approach to our own
libraries seems a natural starting point.

Separating specification and implementations for a few exemplary Idris
libraries would also be a useful proof of concept for the module system:
pushing a more modular approach might expose potential shortcomings of
the current system and suggest avenues for improvement.

Best,
Nicola

[Dean Thompson]

To me, this thread is coming together into a path that seems exciting. I have become very interested in the data science nuance suggested by Kris:

> There’s a distinction between data science being done in an exploratory

> capacity, which is as you say relatively well-served by python, and “data 

> science” operations being integrated into a production system with more

> stringent failure tolerance requirements; this latter space seems to me 

> not at all well-served by any of the environments I’m aware of.

This seems to me to have great synergy with the “self image” of Idris that many of us hold, and that is a recurring theme in this thread: Idris should be fast, safe, rigorous. 

I now find myself excited about a value proposition something like this:

Idris 1.5: the best tool for rigorous, high-performance statistical and machine learning libraries that can be called from other production code in many languages and platforms.

To make progress on that value proposition, here are some things we could work on right now:

• rigorous Idris foundational libraries, as Nicola suggests
• the LLVM backend
• “an optimised backend and runtime for Idris which properly uses uniqueness and/or the information from linear types”, as Tim suggests
• “a typed data frame library providing functionality that is akin to what is available in Python’s “pandas” library, or the R and Julia languages”, as Kris suggests
• a solid version/build tool chain
• easy, reliable use of Idris libraries from Python

Here are some things we’d likely work on down the road:

• easy, reliable use of Idris libraries from other languages
• LLVM on many platforms
• data cleaning libraries, as Gregg suggests
• many statistical and machine learning libraries
• “A replacement for Python/R/Matlab, with strong support for distributed/parallel computing a la Spark or MPI, with outstanding typing, and where I can, if I like, *prove* my results.”, as Bryn suggests

I do hear Pierre:

> I specifically hope that Idris won’t be know for the “best language to do x”.

> I hope it stays general purpose and people will pick it up to have a strongly

> typed language with sane defaults, which they can’t find anywhere else.

> Over time, a natural fit for a specific domain will emerge. 

> At least, that’s what I wish for this language.

But I don’t entirely agree. I wouldn’t want to confine Idris to a single domain. However, I think most languages that succeed in going mainstream are propelled by being the best way to do X:

• COBOL was the best way to build business applications.
• Fortran was the best way to build scientific applications.
• C was the best way to program on Unix.
• C++ was the best way to do OO programming in the C ecosystem.
• JavaScript  was the best way to run code in the browser.
• Java was the best way to build large-scale distributed web and business applications.
• Ruby was the best way to build web apps.

Dean

[Arnaud Bailly]

On Mon, Apr 24, 2017 at 4:40 PM, Dean Thompson <deansher...@gmail.com> wrote:

However, I think most languages that succeed in going mainstream are propelled by being the best way to do X:

• COBOL was the best way to build business applications.
• Fortran was the best way to build scientific applications.
• C was the best way to program on Unix.
• C++ was the best way to do OO programming in the C ecosystem.
• JavaScript  was the best way to run code in the browser.
• Java was the best way to build large-scale distributed web and business applications.
• Ruby was the best way to build web apps.

This may be a kind of after-the-fact rationalisation that has little to do with the intrisic characteristics of each language and all to historical contingencies (e.g. luck). To speak of the languages I know something about:

 - C was the ONLY way to program on Unix for a long time

 - Javascript became the ONLY way to run code in the browser but Flash has been a contender for a long period,

 - Java shifted to server-side code when it became apparent applets won't stick,

 - Ruby was a relatively obscure scripting language until Rails came out and it became fashionable and easy to build web apps with it

 - Python had the luck to have some cool libraries like pandas or scikit and a gentle learning curve that made it easy for non programmers to use it on a daily basis

I would not dare to predict in which direction Idris will find its sweetspot but I am pretty sure it will come as a surprise, if it ever comes.

 

My 2 cts,

Arnaud

[Herwig Habenbacher]

+1

[john NeuMotiveLLC]

Typed, lifted, parallel array language constructs a la APL and J

6 Conclusion
We have given a formal reduction semantics for Iverson’s rank polymorphism which addresses several shortcomings of the model. Remora generalizes automatic operator lifting to include first-class functions and MIMD computation. Embedding the core ideas of APL and J in a setting based on λ-calculus combines the expressive power of both models. Our type system rules out errors due to mismatching argument shapes and still gives the programmer enough freedom to write code whose result shape cannot be determined until run time.

5 Future Work
The transition from a core semantics modeled in PLT Redex to a complete programming system requires a more flexible surface language and a compiler. In moving from the untyped core language to Remora, the added code is mostly type and index applications. Type inference would be necessary in order to make a surface language based on Remora practical. An interesting challenge in this setting is that the different type and index arguments can produce different behavior (e.g., reducing an entire matrix versus reducing its 1-cells). An implementation of Remora could use type information to inform decisions about how to parallelize aggregate operations. With a cost model for analyzing when different cells in an application frame are likely to take significantly different amounts of time, a compiler could choose between statically breaking up a task and leaving the allocation to a work-stealing run-time system. Stream-like computation is often convenient for tasks such as signal processing, and it could be expressed by generalizing array types to allow an unbounded dimension. Implicit lifting still has a sensible meaning, as do foldl, scan, and window. This would allow us to extend Iverson’s rank-polymorphic control mechanism to Turing-equivalent programs requiring while-loop computation (for example, iterating a numeric solver to a given tolerance).

http://www.ccs.neu.edu/home/jrslepak/typed-j.pdf

William J. Bowman‏ @wilbowma Jun 12

Replying to @ezyang

There is some work on types for languages like APL and J that formalizes this sort of thing: http://www.ccs.neu.edu/home/jrslepak/typed-j.pdf …

On Thursday, April 13, 2017 at 12:16:16 PM UTC-6, john NeuMotiveLLC wrote:

SPARK, Ada, Notepad++, Atom b/c formal methods, provability, verification, types

On Thursday, April 13, 2017 at 12:07:19 PM UTC-6, john NeuMotiveLLC wrote:

SPARK, Ada, Notepad++, Atom b/c formal methods, probability, verification, types

[john NeuMotiveLLC]

Also,http://www.cs.ox.ac.uk/people/jeremy.gibbons/publications/aplicative.pdf

[john NeuMotiveLLC]

says: Manuel M T Chakravarty  |  9 August 2017

On Thursday, August 10, 2017 at 12:10:36 PM UTC-6, john NeuMotiveLLC wrote:

Array programming ... is attractive, but [Haskell] can make it hard to know where to start. At some point, we, as a community, need to bring some order into this plethora of options, so that others who want to use [Haskell/Idris] for array programming will see a clear path ahead, but that is a story for another time.

http://www.tweag.io/posts/2017-08-09-array-programming-in-haskell.html

 

[Nickolay Platonov]

Isn't the most obvious continuation: 

Idris 1.5: the best tool for high-assurance programming?

Where "high-assurance programming" is a term, describing software, in which a cost of experiencing a bug is unacceptably high (human safety, high-budged machinery, etc).

If there's no existing niche to fit it, Idris can create one :)

[Ben Hutchison]

At this risk of stating the obvious:

Idris 1.5: the best tool for dependently-typed programming?

I think it's status as the only current "practical" dependently-typed language will be the main draw for people to learn/use Idris for some time to come, rather than a compelling advantage in a particular domain or industry sector.

I think the rate of industry adoption would be boosted by interop with a major ecosystem, with the JVM and JS being the most obvious candidates.

-Ben

--
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+unsubscribe@googlegroups.com.

[Nickolay Platonov]

"dependently typed" is something internal for the programmers community. For the outer world however it's not so meaningful.

--
You received this message because you are subscribed to a topic in the Google Groups "Idris Programming Language" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/idris-lang/xX5rUI1kKMM/unsubscribe.
To unsubscribe from this group and all its topics, send an email to idris-lang+unsubscribe@googlegroups.com.

For more options, visit https://groups.google.com/d/optout.

--

Nickolay

[Alex Silva]

Hallo,

On 02/11/17 14:34, Nickolay Platonov wrote:
>
> On Thu, Nov 2, 2017 at 1:34 AM, Ben Hutchison <brhut...@gmail.com
> <mailto:brhut...@gmail.com>> wrote:
>
>
> I think the rate of industry adoption would be boosted by interop
> with a major ecosystem, with the JVM and JS being the most obvious
> candidates.
>

Although I don't see much point in planning how to go mainstream, in
many cases it happened due to a "killer" application, like what happened
to Ruby because of Rails. Many people hear of Coq because of CompCert.
So in theory you would need just one very popular application to bring a
lot of people onboard.

Cheers,
--
-alex
http://unendli.ch/

[Jackie Kay]

Hey folks,

Idris newbie here, coming from a C++ background.

I came to Idris because I believe dependent types are a key abstraction for practical software engineering patterns. State machines, callback/event handler mechanisms, schedulers, deserialization/parsing... anyone who deals with real-world data and receiving data from a foreign source.

It's hard to sell because the rest of the community doesn't have the right language for it, or the technical understanding to realize that the gains in code expressiveness and performance that are possible with dependent types (I'm not quite sure I do either, just a feeling).

I think the proof-checking capabilities of Idris and the possibility of using dependent types to implement contracts make a strong case for expressive safety-critical code, which will be key as we automate more physical real-world systems.

I also think Idris is well-suited to replacing the sprawling computational graph framework that Tensorflow has become, because graph construction is very naturally expressed a functional paradigm.

Some concrete suggestions (do let me know what existing projects are tackling these problems!):

- A machine learning toolkit (which mostly boils down to tensor operations with constraint optimizations)

- Toolchain support/lightweight runtimes for bare-metal embedded systems

- Image manipulation libraries

- Libraries for motion planning, physical dynamics systems, trajectory planning, and optimal control

- Libraries for hierarchical state machines, MDP's and PoMDPs

- More literature/libraries/documentation on practical safety critical code with Idris (I'm not an expert here)

The difficulty of getting work like this done is that it's really, really hard to find experts in these fields who are also fluent in obscure programming languages like Idris.

However, robotics and AI are the domains that I've spent day-to-day in for the past three years, so I'm likely to project my own domain onto a universally useful abstraction. Also, disclaimer, the views expressed in this email are not the same as my employer's.

Somewhat relatedly, I'm curious to know what the folks on this list think of Rich Hickey's recent inflammatory remarks about static types during his recent Clojure/conj keynote. I personally think that first-class dependent types fix a lot of his problems with static types.

All the best,

Jackie Kay

[Gregg Reynolds]

On Nov 2, 2017 8:34 AM, "Nickolay Platonov" <nick...@gmail.com> wrote:

"dependently typed" is something internal for the programmers community. For the outer world however it's not so meaningful.

best tool for blockchain smart contracts?

[Paul Ivanov]

On Thu, Nov 2, 2017 at 6:06 PM, Gregg Reynolds <d...@mobileink.com> wrote:

On Nov 2, 2017 8:34 AM, "Nickolay Platonov" <nick...@gmail.com> wrote:

"dependently typed" is something internal for the programmers community. For the outer world however it's not so meaningful.

best tool for blockchain smart contracts?

And with that, we've successfully gone from something that had meaning only to the internal programming community, so something where no one knows what it means ;)

Nickolay's earlier suggestion of "high-assurance programming" registers with me, and is what drew me to Idris, along with programming as a dialogue with the machine.

There's a ways to go, though, since I notice that you can end up with both missing cases with programming reported as total, and impossible cases, without getting a warning about that. I was hoping for error message like the kind Elm provides.

In Elm, you typically have a union type of Msg, and an update function that case switches on those types. If you add a new type to Msg, say SomeNewMsg

type Msg

    = Increment

    | Decrement

    | SomeNewMsg

But don't update the cases in update, you will get a MISSING PATTERNS error with the message "This `case` does not have branches for all possibilities...You need to account for the following values:     Main.SomeNewCase Add a branch to cover this pattern!"

Conversely, if you try to use SomeNewMsg without adding it to the Msg union type, you get an error like this "NAMING ERROR ... Cannot find pattern
SomeNewMsg".

Idris handles the first example if you check totality, but there are corner cases such as

Functions with missing case reported as total:

https://github.com/idris-lang/Idris-dev/issues/3942

Function fails to pass totality check if defined using with-block, but passes with case-expression:
https://github.com/idris-lang/Idris-dev/issues/4100

With that, I'd revise the motto to "Idris is the best tool for experimenting with high-assurance program construction"

[Gregg Reynolds]

On Nov 2, 2017 1:58 PM, "Paul Ivanov" <p...@berkeley.edu> wrote:

On Thu, Nov 2, 2017 at 6:06 PM, Gregg Reynolds <d...@mobileink.com> wrote:

On Nov 2, 2017 8:34 AM, "Nickolay Platonov" <nick...@gmail.com> wrote:

"dependently typed" is something internal for the programmers community. For the outer world however it's not so meaningful.

best tool for blockchain smart contracts?

And with that, we've successfully gone from something that had meaning only to the internal programming community, so something where no one knows what it means ;)

Victory! (All that matters is impressive buzzword compliance.)

Nickolay's earlier suggestion of "high-assurance programming" registers with me, and is what drew me to Idris, along with programming as a dialogue with the machine.

my quibble with that is that it's too loose.  how high is "high"?  fwiw i prefer some variant of "certified". people unnerstand that. a vendor could also offer warranties.

...

With that, I'd revise the motto to "Idris is the best tool for experimenting with high-assurance program construction"

"experimenting" = kiss of death.  why would i use an experimental language if i want "best"? howsabout "Idris is the best language for building practical software whose correctness is certifiable"?

[Gregg Reynolds]

make that "machine-certifiable" or similar.

[zenten]

What I'm trying to see is if Idris would be useful in areas where they're making due with bug fixes and existing levels of testing, but it would be more profitable to use Idris.

--

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.

[Gregg Reynolds]

On Nov 2, 2017 8:34 AM, "Nickolay Platonov" <nick...@gmail.com> wrote:

"dependently typed" is something internal for the programmers community. For the outer world however it's not so meaningful.

my guess is that it's not so meaningfull even for the vast majority of programmers atm.

[stewart mackenzie]

Hi folks,

In line with the tensorflow comment, I'm currently working on
integrating Idris into Fractalide - github.com/fractalide/fractalide

Fractalide implements the Flow-based Programming paradigm, a dataflow
graph like DSL. Where nodes represent computations and edges dependent
types passed over a message passing medium from node to node.

My goal is to eventually create a platform that allows programmers to
create reusable, reproducible and composable components that compose
into an executable.
These components can then be made available on a marketplace.
Programmers may then charge money for their components, which may then
be composed into other subgraphs. (the marketplace is currently
vapourware atm)
When an end user purchases that subgraph every programmer that created
a component in the subgraph gets compensated.

I rely heavily on the nix package manager to wrap every node in the
system and keep dependencies sane. Indeed it's through nix that i'm
able to manage the lifecycles of every node in the system without
going insane.

Currently the system is based on Rust, but I'm ramping up for a front
end in the browser. Idris was too appealing so I'm using it, it'll
probably fail due to my incompetence, but it seems really fun.

So far I've got nix building transitive dependencies of idris
libraries and can pull in the edge dependent types into the agent at
build time.
I can also use the repl inside a nix-shell and works equally well
within idris-modes (with a caveat).
I still need to implement the scheduler and agent code, then I'll
really need help from the Idris community to help build out the
hundreds of components to make it into a functional system

Here's a quick description of what works so far:
https://github.com/fractalide/fractalide/tree/master/nodes/idr

/sjm

[Paul Ivanov]

"experimental" because that's the honest assessment of the maturity / stability of the language implementation at the moment. There are still plenty of rough edges.

--

                   _

                  / \

                A*   \^   -

             ,./   _.`\\ / \

            / ,--.S    \/   \

           /  `"~,_     \    \

     __o           ?

   _ \<,_         /:\

--(_)/-(_)----.../ | \

--------------.......J

Paul Ivanov
http://pirsquared.org | GPG/PGP key id: 0x0F3E28F7

[Alex Silva]

Hallo,

On 02/11/17 19:58, Paul Ivanov wrote:
>
> Idris handles the first example if you check totality, but there are
> corner cases such as
>
> Functions with missing case reported as total:
> https://github.com/idris-lang/Idris-dev/issues/3942
>
> Function fails to pass totality check if defined using with-block, but
> passes with case-expression:
> https://github.com/idris-lang/Idris-dev/issues/4100
>
> With that, I'd revise the motto to "Idris is the best tool for
> experimenting with high-assurance program construction"
>

Bugs are annoying, yes, but I'd be more worried about design flaws. Bugs
eventually get fixed. Incidentally, this is an argument for bringing in
more people: The bugs get fixed faster.

[Drill Bear]

At the risk of sounding facetious, I think the best audience to "sell" a programming language to is programmers. Idris might be a difficult sell in the same way as Haskell - "But what is Haskell actually good for?" is an amusingly common question from programmers of other (more mainstream) languages, and there's no specific answer. The most popular languages I can name in 15 seconds were clearly created with a particular applicable strength in mind from day 1. With that, I don't think trying to pick a niche for Idris after version 1.0 will necessarily succeed. It should happen organically (as others have discussed, Python's relationship with data science come to mind).

I do agree with another reply that "dependently-typed" probably doesn't mean all that much to many programmers in the first place. But Idris has a lot of features that blow other languages away: implicit conversion functions, overloading, extensible syntax, a great REPL - all great helps that I miss when I have to use something else, and I haven't even touched features like idiom brackets and all the proof-related stuff.
One of the hairiest thing I wrote in Haskell was part of an EDSL where the user could define and use functions of arbitrary arity. It took the best part of a week to figure out exactly how to massage type classes to do what I wanted. I did a similar thing for Idris and it took a single evening using overloaded list syntax and 100% fewer LANGUAGE pragmas, and I didn't even realise I'd used dependent types until it was finished!
To me, at least, Idris is Haskell with added ergonomics. Dependent typing is the icing on the cake - it bridges the divide between the type world and the value world. A beginning user might try, say, using a function in a type signature and would need to learn why that doesn't work in Haskell (I know I did), but there is no such problem in Idris. In that sense dependent typing is not as much an added feature as it is the removal of a restriction.

What I'm saying is, Idris 1.5 could be the most accessible tool for (functional, type-safe, dependable) general programming. I think that to try to make a language "succeed" when success is defined by the size of the user base, it's prudent to focus on accessibility rather than going for a particular subset of use cases. Another 4 point releases is plenty of time to increase ease of use and improve ergonomics even further. If Idris 1.5 is easier to learn, more people would use it, leading to wider adoption in The Industry. After all, the software industry is made of people: I would rather use a language because other people found it useful, not because management were sold on its business benefits.

Go's success is aided in no small part by both how quickly you can start writing meaningful programs, and its place in industry ("Google use it, so we should too!").
With Rust, their community team have done a great job helping the Rust community grow to be vibrant and diverse. But the language might have needed that - after all, its restrictions are deliberate and somewhat tricky. A language like Idris 1.5 might not even need that, as its user base could grow more organically thanks to lower barriers to entry.

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.

--
You received this message because you are subscribed to a topic in the Google Groups "Idris Programming Language" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/idris-lang/xX5rUI1kKMM/unsubscribe.

To unsubscribe from this group and all its topics, send an email to idris-lang+...@googlegroups.com.

For more options, visit https://groups.google.com/d/optout.

--

Nickolay

[John Motsinger]

Tool nivana: a type-total, component-ized incrementally-compiled Blodwen/Idris/Haskell, Luna-Lang, visual/textual, f-array GPU https://t.co/7AHJXm7BDi Atom(?) plug-in; moonshot https://t.co/mCp28GJ9mF

[0nkery]

What about Erlang/Elixir ecosystem?

There was a work to embed Haskell inside of BEAM (https://wiki.haskell.org/Yhc/Erlang/Proof_of_concept) but researchers faced these lazy-eager problems.

Since Idris is strict by default it would be easier to embed it in this ecosystem than Haskell [0]. Also consider verified OTP primitives like gen_server or gen_fsm or gen_event (even partly verified) using 

some flavor of pi-calculus [1].

[0] There WAS a work for Erlang backend for Idris - https://github.com/lenary/idris-erlang.

[1] Similar Coq library - https://github.com/amutake/actario.

четверг, 13 апреля 2017 г., 21:35:46 UTC+7 пользователь Dean Thompson написал: