33

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?

András Kovács
  • 29,931
  • 3
  • 53
  • 99
  • 14
    It's on my TODO list - normally things move up the TODO list if somebody else asks about them, so just asking this is one way to help remedy it :). Surprisingly, there hasn't really been much demand for this, though obviously it would be nice. There is some trickiness in getting implicit arguments right, so we've taken a pretty simple approach for now. Type classes are first class, so there is also a clumsy way to do class constraints - treat them as normal function arguments, and use '%instance' to find the instance explicitly. – Edwin Brady Apr 05 '14 at 15:29
  • @EdwinBrady thanks, I accept this as an answer (or I'd do so were it an answer). – András Kovács Apr 05 '14 at 19:11
  • It doesn't yet feel like a proper answer... I'll get back to you soon hopefully! – Edwin Brady Apr 06 '14 at 00:17
  • Part 4 of my [question on the google group](https://groups.google.com/d/msg/idris-lang/VAbWdO2K9tQ/4dGxMAKBGk8J), is similar to this SO question, cross linking for future readers. – Davorak Jul 22 '14 at 01:42

1 Answers1

23

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

Edwin Brady
  • 4,546
  • 1
  • 22
  • 14