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
As you describe, singleton types are those which have only one value (let’s ignore ⊥ for the moment). Thus, the value of a singleton type has a unique type representing the value. The crux of dependent-type theory (DTT) is that types can depend on values (or, said another way, values can parameterise types). A type … 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
There are at least two examples in the paper itself: “1. Introduction” says: “for example, we might be able to ensure [at compile time] that an alleged red-black tree really has the red-black property”. “2.1 Promoting datatypes” discusses length-indexed vectors (that is, vectors with compile-time “index out of bounds” errors). You can also take a … Read more
Liquid Haskell has totality checking: https://github.com/ucsd-progsys/liquidhaskell#termination-check By default a termination check is performed on all recursive functions. Use the no-termination option to disable the check liquid –no-termination test.hs In recursive functions the first algebraic or integer argument should be decreasing. The default decreasing measure for lists is length and Integers its value. (I included screenshot … Read more
To my mind, the value of containers (as in container theory) is their uniformity. That uniformity gives considerable scope to use container representations as the basis for executable specifications, and perhaps even machine-assisted program derivation. Containers: a theoretical tool, not a good run-time data representation strategy I would not recommend fixpoints of (normalized) containers as … 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
Axiom K is also called the principle of uniqueness of identity proofs, and it is an axiom about the nature of the identity type in Martin-Löf’s dependent type theory. This type doesn’t exist (and in fact cannot be defined) in simpler type theories such as System F, so that is probably the reason why you … 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