Closed edwinb closed 2 years ago
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.
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
@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.
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.
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.
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.
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.
Also, it'll be good if we have a doc for the std library, which makes it more friendly for the mass programmers.
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.
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.
@ohad @ShinKage Wow, thanks a lot.
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.
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.
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.
Add time complexity & space complexity descriptions in the :doc
command for REPL, since most of the time programmers care about it.
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.
Proposal: An import qualified
feature analogous to Haskell's.
Background:
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:
import X hiding y
is also helpful, so optionally it would be nice to add that too.
- 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.
I'll close this as it's a pot pourri of distinct suggestions, some of which have been addressed already.
Issue by edwinb Thursday Jul 18, 2019 at 17:58 GMT Originally opened as https://github.com/edwinb/Idris2-boot/issues/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!