Idris reimplementation

[Edwin Brady]

Hi all,
You might be interested to know that I'm working on a complete reimplementation of Idris (because adding new features was just getting too hard with the Ivor/Idris design, among other reasons. Plan to throw one away, they say...). You can follow it at:

https://github.com/edwinb/MiniIdris

Or read a bit more at:

http://edwinb.wordpress.com/2011/10/10/idris-mk-ii/

There's no with rule, or IO (hence compilation...) yet, but they won't be long. On there other hand, most of the basic language is there, and there are now where clauses (that's one of the things that was far too complicated to add in the old version but was easy in the new).

If you do have a go with it, let me know how you get on. Also, since it's at an early
stage, now is probably a good time to send feature requests before they get too hard to do :).

Edwin.

[Cezar Ionescu]

Hurray, hurray, "where" clauses!

Feature requests:

- records

- Gofer- or Hugs-like interface (especially calling the editor from
the prompt)

- modules (less important if we have records, but anyway would be
nice)

Thanks for all the work!

Best,
Cezar.

[DirkU]

Hello,

I've tried to play a bit with MiniIdris. It did compile (using GHC
7.0.2) but when trying ti run miniidirs I always get the error:

miniidris: user error (Can't find import list)

Did I miss something, or is it a bug to fix?

Dirk

[Edwin Brady]

Hi Dirk,
That was me forgetting to add lib/list.idr to the repository. If you get the latest version it should be fine.

Edwin.

[Dirk Ullrich]

Hi Edwin,

2011/10/15 Edwin Brady <edwin...@gmail.com>:

> Hi Dirk,
> That was me forgetting to add lib/list.idr to the repository. If you get the latest version it should be fine.
>

I already had `lib/list.idr' :-( I do net yet understand what should
happen with these *.idr files during installation. Should they
'compiled in' in some way? Or must they be placed somewhere in the
installation such that can be found by the binary? If yes, where?

I ask these questions since I couldn't figure out answers from
studying the make and cabal files.

Dirk

[Dirk Ullrich]

Hi Edwin,

2011/10/15 Dirk Ullrich <dirk.u...@googlemail.com>:

> Hi Edwin,
>
> 2011/10/15 Edwin Brady <edwin...@gmail.com>:
>> Hi Dirk,
>> That was me forgetting to add lib/list.idr to the repository. If you get the latest version it should be fine.
>>
> I already had `lib/list.idr' :-( I do net yet understand what should
> happen with these *.idr files during installation. Should they
> 'compiled in' in some way? Or must they be placed somewhere in the
> installation such that can be found by the binary? If yes, where?
>
> I ask these questions since I couldn't figure out answers from
> studying the make and cabal files.
>

sorry for the noise in my last e-mail. After learning something more
about how cabal works and studying the MiniIdris code I figured out
the answers to my questions by myself: The *.idr files are loaded via
`prelude.idr' during miniidris' start. (And the are properly placed,
by `cabal install', into a cabal's $datadir/$datasubdir. So ervery is
okay but one: `prelude.idr' tries to import `vect', and a `vect.idr'
is missing yet in Git, right?

Dirk

[Edwin Brady]

On 15 Oct 2011, at 20:10, Dirk Ullrich wrote:

> sorry for the noise in my last e-mail. After learning something more
> about how cabal works and studying the MiniIdris code I figured out
> the answers to my questions by myself: The *.idr files are loaded via
> `prelude.idr' during miniidris' start. (And the are properly placed,
> by `cabal install', into a cabal's $datadir/$datasubdir. So ervery is
> okay but one: `prelude.idr' tries to import `vect', and a `vect.idr'
> is missing yet in Git, right?

Oops, looks like you're right... fixed now. I've even checked on a remote machine to be sure I haven't missed anything!

But this is the idea, yes - there is a prelude.idr, in lib/, along with some other .idr files, all of which are installed by a cabal install. If you do a 'make', then these get checked too.

By the way, at the moment, you will also need the latest EpiVM from git, but I will upload a new version to hackage soon.

Edwin.

[Dirk Ullrich]

Hallo Edwin

2011/10/16 Edwin Brady <edwin...@gmail.com>:
[...]

> By the way, at the moment, you will also need the latest EpiVM from git, but I will upload a new version to hackage soon.
>
> Edwin.

this is no problem for me since for Epic and some other stuff (like
Agda, for instance) I use the development code anyway. I've noticed
the hello world stuff from the Idris tutorial is already working!

By the way I have an enhancement proposal: What's about a foreign
language interface in Whitespace to Idris that brings the power of
dependent types to Whitespace? A friend of mine already suggested a
suitable name for this enhanced Whitespace: Whitespace-tab-tab.

Dirk

[Edwin Brady]

On 17 Oct 2011, at 11:43, Dirk Ullrich wrote:

> Hallo Edwin
>
> 2011/10/16 Edwin Brady <edwin...@gmail.com>:
> [...]
>> By the way, at the moment, you will also need the latest EpiVM from git, but I will upload a new version to hackage soon.
>>
>> Edwin.
> this is no problem for me since for Epic and some other stuff (like
> Agda, for instance) I use the development code anyway. I've noticed
> the hello world stuff from the Idris tutorial is already working!

Yes, the compiler is up and running (although not optimising at all yet) and there's a bit of syntactic sugar for pairs and syntax declarations. I'm not *quite* ready to say it's possible to do serious work in it yet, because I need to sort out a unification problem first, but it's not far off...

> By the way I have an enhancement proposal: What's about a foreign
> language interface in Whitespace to Idris that brings the power of
> dependent types to Whitespace? A friend of mine already suggested a
> suitable name for this enhanced Whitespace: Whitespace-tab-tab.

:-). Any volunteers?

Edwin.