Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Doing rank-n quantification in Idris

I can only do rank-n types in Idris 0.9.12 in a rather clumsy way:

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

I need the underscores wherever there's a type application, because Idris throws parse errors when I try to make the (nested) type arguments implicit:

tupleId : ({a : Type} -> a -> a) -> (a, b) -> (a, b) -- doesn't compile

A probably bigger issue is that I can't do class constraints in higher-rank types at all. I can't translate the following Haskell function to Idris:

appShow :: Show a => (forall a. Show a => a -> String) -> a -> String
appShow show x = show x

This also prevents me from using Idris functions as type synonyms for types such as Lens, which is Lens s t a b = forall f. Functor f => (a -> f b) -> s -> f t in Haskell.

Any way to remedy or circumvent the above issues?

like image 860
András Kovács Avatar asked Apr 05 '14 11:04

András Kovács


1 Answers

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...

like image 70
Edwin Brady Avatar answered Oct 07 '22 22:10

Edwin Brady