Feature requests and proposals

[edwinb]

Issue by edwinb
Thursday Jul 18, 2019 at 17:58 GMT
Originally opened as edwinb/Idris2-boot#30

---

If you have a feature request or proposal, or if you're looking for a place to get started contributing to Idris 2, please take a look at https://github.com/idris-lang/Idris2/wiki/Contributions-wanted, or at https://github.com/idris-lang/Idris2/blob/master/CONTRIBUTING.md

At the moment, since it's (mostly) only me working on the project, in about half my time, this is mainly in an effort to prevent the issue tracker for getting out of control, and making sure that I can keep on top of the most important bugs.

Please feel free to discuss proposals via the wiki or the mailing list, however!

[edwinb]

Comment by mrkgnao
Tuesday Mar 10, 2020 at 01:29 GMT

---

Added a note about the possibility of modifying the core type theory to track usage in types on the wiki.

[andylokandy]

Support intrusive unit test framework like Rust, who can run tests on private functions.

Instead of providing a first-class test framework integrated into the language, we can make use of the Elab Reflection for the test framework to extract all test functions in the source. That requires the Elab Reflection to have the ability to search through modules including the private items and to provide a custom notation mechanism on items.

For example:

private
foo : Int -> Int
foo n = n + 1

%test
testFoo : IO ()
testFoo = assert $ foo 1 == 2

With this mechanism, we can also support the benchmark framework.

Ps: Doc-test is also good to have.

[gallais]

You can already write these kind of unit tests by forming the type foo 1 = 2
and telling idris the proof out to be Refl.

We do an (advanced) version of that in tparsec by running our parser examples
at compile time: https://github.com/gallais/idris-tparsec/tree/master/src/Examples

[andylokandy]

@gallais Interesting idea! But I think it's insufficient, because, for example, the Path I added into the compiler made use of System.Info.os, and that could not be decided in compile-time; on the performance aspect, it's too much to run all tests in every compilation when we have large test cases.

[polendri]

Would it make sense for there be a Cast Char Nat implementation in order to better support creating predicates on Char?

Char currently only has casts to Int and to Integer. I'm not familiar with the data representation of Char, but UTF-8 code points are unsigned so it seems to me (uneducated in the Idris internals as I am) that it should be possible to do a performant, lossless cast. In Rust for example, `'x' as u32' is valid.

My motivation is to be able to write predicates for Char like

Lowercase : Char -> Type where
  IsLowercase : (c : Char) -> (LTE 'a' c) -> (LTE c 'z') -> Lowercase c

isLowercase : Char -> Dec Lowercase where
isLowercase c = ?impl

Currently, as far as I know, the only way to do this sort of thing on Char is to convert it to a sum type that covers the character set being considered (e.g. ASCII = ATab | ASpace | ...). Once it's in that form, isLowercase can be implemented with pattern matches on every single enum value, but that's a mess if a large character set is being considered (and presumably it's very slow as well). If Char can be cast to Nat in a performant way however, it should be possible to implement an LTE predicate for it and do efficient range comparisons for chars.

What I'm ultimately hoping for is to be able to write predicates for string validation/parsing, e.g. to validate that a string argument has the shape [a-z][a-zA-Z0-9]*.

Edit: In case it's relevant to anyone reading this, it appears Char -> Nat and Nat -> Char casts were implemented in #1629.

[workingjubilee]

This is possible in Rust because char is defined as a Unicode Scalar Value, which definitionally is up to 4 bytes. This may prove unfortunately Entertaining to implement across multiple backends if certain backends disagree on encoding of Char. Judging by other issues, I see that there is at least some usage of a JavaScript backend. As JS Strings must be indiced base on UTF-16, the codegen may have to be adjusted. However, I did enough meandering to at least recover some evidence that it uses ECMAScript 2015 fromCodePoint and codePointAt functions, so it probably is indeed expressible as a u32.

Idris2/src/Compiler/ES/ES.idr

Lines 261 to 264 in f64163d

	jsOp (Cast IntType CharType) [x] = pure $ "String.fromCodePoint(" ++ fromBigInt x ++ ")"
	jsOp (Cast IntegerType CharType) [x] = pure $ "String.fromCodePoint(" ++ fromBigInt x ++ ")"
	jsOp (Cast CharType IntType) [x] = pure $ toBigInt $ x ++ ".codePointAt(0)"
	jsOp (Cast CharType IntegerType) [x] = pure $ toBigInt $ x ++ ".codePointAt(0)"

[ziman]

Also, I'd say Nat is not suitable for representation of Char values. Nat is not a general-purpose numeric type. It has a unary structure, which is suitable for reasoning about sizes of data structures but not suitable for expressing plain numbers such as unicode code points. The Idris equivalent of u32 is Bits32; it has the right (un)signedness, and (mostly) the right range (while Nat is unbounded).

Since Char has an Ord instance, too, you can also write

Lowercase : Char -> Type
Lowercase c = ('a' <= c && c <= 'z') === True

or something similar to get that predicate.

[glyh]

I've found that there're some extensions for different IDEs developed. But I think it'll be better if we have an LSP, so that we can just implement the language detail regardless of the IDE.

[glyh]

Also, it'll be good if we have a doc for the std library, which makes it more friendly for the mass programmers.

[ohad]

Also, it'll be good if we have a doc for the std library, which makes it more friendly for the mass programmers.

We (temporarily) have this: https://www.idris-lang.org/pages/idris-2-documentation.html
I think it's not yet linked to from the main page.

[ShinKage]

I've found that there're some extensions for different IDEs developed. But I think it'll be better if we have an LSP, so that we can just implement the language detail regardless of the IDE.

We started working on an LSP server implementation here https://github.com/idris-community/idris2-lsp, it is practically on parity with old editing commands, minus semantic highlighting which has been recently merged in the compiler, but we are working on it.

[glyh]

@ohad @ShinKage Wow, thanks a lot.

[glyh]

Do we have FFI with languages other than C (for example, haskell, rust)? I found there's only example of C on the FFI page.

[buzden]

Do we have FFI with languages other than C (for example, haskell, rust)? I found there's only example of C on the FFI page.

There are FFIs with at least scheme (chez, racket) and javascript. Anyway, they are managed by each codegen separately AFAIK. You can grep the libs folder for %foreign pragma to search for examples.

[gallais]

This discussion should probably go somewhere else than the bug tracker.
The mailing list and the discord server are much more suited to this Q&A
style discussion on Idris & its features.

[glyh]

Add time complexity & space complexity descriptions in the :doc command for REPL, since most of the time programmers care about it.

[fogti]

It would be interesting to have type class constrained specialization equivalence (a term I just made up, hopefully not completely un-understandable), e.g. see also / source

Functor m <=> GenFunctor Prelude.id m where
  map = gmap

which would mean that an implementation of either Functor m or GenFunctor n m (with Prelude.id : n or similiar) imply an implementation of the other one.

[polendri]

Proposal: An import qualified feature analogous to Haskell's.

Background:

• Haskell's import syntax
• A matching feature request from the Idrs 1 repo

Motivation: The existing import Foo as F functionality is, on its own, only a shorthand to avoid typing out a full path when disambiguating names (since everything in Foo gets imported bare in addition to under F.). import qualified Foo as F makes it possible to selectively access names in a module, potentially avoiding a tedious amount of disambiguation.

Other considerations:

• I'm not familiar with the module system, so I'm not sure whether there's some reason why this might be difficult. If it's not out of reach of a first-time contributor (with some direction), and if it's a welcome feature, I'd be interested in tackling it.
• The syntax doesn't need to be like Haskell of course, but I see no reason to deviate from it.
• The import X hiding y is also helpful, so optionally it would be nice to add that too.

[buzden]

• The import X hiding y is also helpful, so optionally it would be nice to add that too.

Have you considered the %hide feature of the language? It is not really documented but you can how it is used.

[gallais]

I'll close this as it's a pot pourri of distinct suggestions, some of which have been addressed already.