Doing rank-n quantification in Idris

by

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 -> String
appShow s x = s x

AppendType : Type
AppendType = {a, n, m : _} -> Vect n a -> Vect m a -> Vect (n + m) a

append : AppendType
append [] ys = ys
append (x :: xs) ys = x :: append xs ys

tupleId : ({a : _} -> a -> a) -> (a, b) -> (a, b)
tupleId f (a, b) = (f a, f b)

Proxy  : Type -> Type -> Type -> Type -> (Type -> Type) -> Type -> Type

Producer' : Type -> (Type -> Type) -> Type -> Type
Producer' a m t = {x', x : _} -> Proxy x' x () a m t

yield : Monad m => a -> Producer' a m ()

The main constraint at the minute is that you can’t give values for implicit arguments directly, except at the top level. I’ll do something about that eventually…

Leave a Comment