Using Hackage libraries from Idris?

[Allan J Cooper]

I'm new to Idris and it's a beautiful language (and Type Driven Development with Idris is a beautiful book!) 

But to use Idris as a general purpose programming language, realistically i need to leverage Hackage. The biggest reason is that Haskell already has wrappers for most of the important c libraries. 

I haven't been able to locate the discussion of this issue. Is there some major problem concerning how this would be abstracted? Are there fundamental issues that would prevent access to Hackage from Idris, or at least a subset of Hackage that conforms to some appropriate standards? At worst, could there be something like an FFI or something like automatic translation of Haskell to idris? 

Thanks!

Allan 

[Shea Levy]

Hi Allan,

While the Idris compiler itself is (for now!) a Haskell program, Idris
programs are not linked against the GHC runtime and Idris is quite a
different language from Haskell. Calling a haskell library from Idris
would have to go via the C ffi much like calling haskell from, say,
python. If you care about wrapping C libraries, it makes more sense to
just go straight to those libraries.

Thanks,
Shea

[Zoltán Tóth]

On Thursday, December 8, 2016 at 6:51:30 PM UTC+1, Allan J Cooper wrote:

Are there fundamental issues that would prevent access to Hackage from Idris

Idris is not compatible with Haskell at all. One fundamental reason is that Haskell is practically lazy but Idris is eager.
 

At worst, could there be something like an FFI or something like automatic translation of Haskell to idris? 

No automatic translation either.

Idris has some C FFI, but i found it incomplete and not documented. I hope that the developers will address this so that the community will be able to wrap C libraries easily.

[Edwin Brady]

On 08/12/2016 19:01, Zoltán Tóth wrote:
> Idris has some C FFI, but i found it incomplete and not documented. I
> hope that the developers will address this so that the community will be
> able to wrap C libraries easily.

I was about to point at the docs on http://docs.idris-lang.org/ but then
I looked and discovered that they documented the old, no longer
existing, version! So we'd better fix that.

I ask more in hope than expectation, but is anyone willing to bring it
up to date? I don't really have time at the moment, but I'll do it
eventually if nobody else can. You'd be welcome to copy anything you
like from https://eb.host.cs.st-andrews.ac.uk/drafts/compile-idris.pdf

Edwin.

[Colin Adams]

I might have a go (though I haven't done any Idris programming since May).

Email me in a week's time if no-one else has taken it up.

[Allan J Cooper]

Hi Colin! Ping! 

It does seems as though you and Niklas have the most experience to date, so could best explain how FFI works in practice, at least for C! I would guess the most obvious questions people will have are how to handle c structs and memory allocation, and perhaps an example of how to create a wrapper using some sort of universe pattern to impedance-match between whatever model the Idris code is creating and what the C library model was. 

Another question that has come up a tangentially is how to manage a large block of memory if required, as might happen in wrapping a scientific library or performing file reads eagerly. One might imagine Idris in the role of the "specification language" and foreign functions are viewed as special purpose "hardware", for instance. As far as I understand, UniquenessTypes and LinearTypes could be used to accomplish this type of resource management nicely (though might require some kind of primitive type to represent, say, a block of memory or resources such as a gpu). 

Allan 

[Colin Adams]

On Mon, 9 Jan 2017 at 22:03 Allan J Cooper <allanj...@gmail.com> wrote:

Hi Colin! Ping! 

That was a long week!

And I've gotten busy with something else in the meantime. Still, I can probably find enough time in the next few weekends to do something useful. 

 

It does seems as though you and Niklas have the most experience to date, so could best explain how FFI works in practice, at least for C! I would guess the most obvious questions people will have are how to handle c structs and memory allocation, and perhaps an example of how to create a wrapper using some sort of universe pattern to impedance-match between whatever model the Idris code is creating and what the C library model was. 

I can certainly do that. The only question I have is:

Why? Isn't this already documented? I learned partly from reading the documentation, and partly from questioning Niklas. And I thought I had updated the documentation in response to what i learned from Niklas.

So, which pages (URLs please) need updating.

Another question that has come up a tangentially is how to manage a large block of memory if required, as might happen in wrapping a scientific library or performing file reads eagerly. One might imagine Idris in the role of the "specification language" and foreign functions are viewed as special purpose "hardware", for instance. As far as I understand, UniquenessTypes and LinearTypes could be used to accomplish this type of resource management nicely (though might require some kind of primitive type to represent, say, a block of memory or resources such as a gpu). 

That might be beyond me. Not sure.

 

Allan 

On Thursday, December 8, 2016 at 10:44:11 PM UTC-8, Colin Adams wrote:

I might have a go (though I haven't done any Idris programming since May).

Email me in a week's time if no-one else has taken it up.

On Thursday, 8 December 2016 19:20:53 UTC, Edwin Brady wrote:

On 08/12/2016 19:01, Zoltán Tóth wrote:
> Idris has some C FFI, but i found it incomplete and not documented. I
> hope that the developers will address this so that the community will be
> able to wrap C libraries easily.

I was about to point at the docs on http://docs.idris-lang.org/ but then
I looked and discovered that they documented the old, no longer
existing, version! So we'd better fix that.

I ask more in hope than expectation, but is anyone willing to bring it
up to date? I don't really have time at the moment, but I'll do it
eventually if nobody else can. You'd be welcome to copy anything you
like from https://eb.host.cs.st-andrews.ac.uk/drafts/compile-idris.pdf

Edwin.

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

[Colin Adams]

Also, which branch should I be updating? (I mean, which branch should I create a new branch off, for my updates?)

[Allan J Cooper]

Hi Colin! 

Not sure how to answer the branch question, but I definitely found there is already much more documentation on FFI than I had realized. In fact going through this I would say that all the documentation would do better to be reorganized and I'll open up a separate issue for that. 

Speaking to the existing FFI documentation, there are now 4 hits if you search FFI in ReadTheDocs. Here are my initial thoughts on how they might be reorganized, what do you think? First, I'd say all the FFI information now should be collected into one place, under Language Reference. 

ASIDE: I think it would be awesome to have a tutorial "How to wrap" guiding us through how to make wrappers for one or more of the many important C libraries. That would also provide a recipe to jump start the Idris library wrapping industry as has been so useful making Haskell a practical programming language. 

Specifics on the current FFI documentation: 

1. Docs » Language Reference » New Foreign Function Interface 

http://docs.idris-lang.org/en/latest/reference/ffi.html?highlight=FFI

-- should be the main topic header for FFI

-- the word "New" should be dropped, there's no old one

2. Docs » Language Reference » Miscellaneous / C Heap 

http://docs.idris-lang.org/en/latest/reference/misc.html?highlight=FFI#c-heap

-- awesome stuff, but should be merged into Reference.FFI where at the very least the context is clear, otherwise we should describe the general importance of memory management primitives (and perhaps "idrisize" that with uniqueness types or some cool memory abstraction). 

3. Docs » Language Reference » Miscellaneous / Type Providers

http://docs.idris-lang.org/en/latest/guides/type-providers-ffi.html

-- again, this purports to be general but the context is really FFI_C so I think it belongs in Reference.FFI. If and when an expanded tutorial discusses Type Providers more generally that tutorial can point to the reference material. 

4. Docs » The Idris Tutorial » Miscellany
http://docs.idris-lang.org/en/latest/guides/type-providers-ffi.html?highlight=FFI

-- This seems to be the only source for the material it contains, for instance Include and Linker Directives, so although it's written in tutorial style I think it belongs in reference! Also, the material here is "reference" not "tutorial" in nature, because it isn't telling how some exemplary thing was accomplished, it's documenting the full range of things that are possible. 

5. (not sure)

libs/contrib/CFFI/Memory.idr

-- I'm not sure i understand this completely, but there seems to be some material here (malloc / calloc) that doesn't appear in the documentation. 

6. Edwin's earlier post on this thread. 

-- The compile-idris paper section 4 describes general FFI (not only to C) and provides / proposes some additional abstractions by which FFI might be made to look and behave more succinctly in Idris. 

-- to some extent the chapter is suggestive of what might be done rather than how Idris actually works today, so is a development or even a small research project 

-- I don't understand things well enough to do much more than summarize. If we have nothing better we could just do that for now, perhaps add a final section called "FFI to Languages besides C, with some suggested abstractions". 

-- we could certainly add a reference to the paper, after a short summary, which might be fine for release 1.0. 

Allan