We say Idris has strict evaluation, but this is for its run-time semantics. Being a fully dependently typed language, Idris has two phases where it evaluates things, compile-time and run-time. At compile-time it will only evaluate things which it knows to be total (i.e. terminating and covering all possible inputs) in order to keep type … Read more
Due to laziness, Haskell types are both inductive and coinductive, or, there is no formal distinguishment between data and codata. All recursive types can contain an infinite nesting of constructors. In languages such as Idris, Coq, Agda, etc. a definition like ones = 1 : ones is rejected by the termination checker. Laziness means that … Read more
I’ve just implemented this in master, allowing implicits in arbitrary scopes, and it’ll be in the next hackage release. It’s not well tested yet though! I have at least tried the following simple examples, and a few others: appShow : Show a => ({b : _} -> Show b => b -> String) -> a … Read more
Yes, you’re right to observe that the types versus values distinction in Idris does not align with the compiletime-only versus runtime-and-compiletime distinction. That’s a good thing. It is useful to have values which exist only at compiletime, just as in program logics we have “ghost variables” used only in specifications. It is useful also to … Read more
When you see a family of types, you may wonder whether each of the arguments it has are parameters or indices. Parameters are merely indicative that the type is somewhat generic, and behaves parametrically with regards to the argument supplied. What this means for instance, is that the type List T will have the same … Read more
The confusion arises from using similar terminology for the structure of a Σ type and for how its values look like. A value of Σ(x:A) B(x) is a pair (a,b) where a∈A and b∈B(a). The type of the second element depends on the value of the first one. If we look at the structure of … Read more
Edwin Brady has a repo full of demos at https://github.com/edwinb/idris-demos. Among other things, it has a playable space invaders game, written using SDL bindings, Effects, and the !-effect syntax (basically an alternate syntax to do-notation / >>=). Also, we attempt to maintain a listing of some available libraries on the wiki: https://github.com/idris-lang/Idris-dev/wiki/Libraries
I would highly recommend Software Foundations. This book is quite good at introducing you to Coq one step at a time. There is a lot of theorem proving, yes, but that’s part of the deliciousness of dependent types. It’s a great feeling when the line between “programming” and “proving” starts to blur. I’m lacking in … Read more
Suppose we input n :: Int at runtime from STDIN. We then read n strings, and store them into vn :: Vect n String (pretend for the moment this can be done). Similarly, we can read m :: Int and vm :: Vect m String. Finally, we concatenate the two vectors: vn ++ vm (simplifying … Read more
This is the static, type-system version of, How do you tell that your tests are correct? The only answer I can honestly give is, yes, the more complex and unwieldy your specification, the more likely you are to have made a mistake. You can mess up in writing something in a type theoretic formalism just … Read more