Higher-kinded interfaces

[duvenaud]

I'm trying to implement the Functor interface in Dex, to let me map over more types of data structures. However, it seems like Dex is missing syntax to specify that it generalizes over type constructors, not just types.

I think the Idris implementation is satisfactory:

interface Functor (f : Type -> Type) where
    map : (func : a -> b) -> f a -> f b

But the equivalent in Dex doesn't work:

interface Functor (t:Type->Type)
  map' : a:Type ?-> b:Type ?-> eff:Effects ?-> (a->{|eff} b) -> (t a) -> {|eff} (t b)

gives

Parse error:30:20:
   |
30 | interface Functor (t:Type->Type)
   |                    ^
unexpected 't'
expecting symbol name or type constructor parameter

and other variations give similar errors.