Using interfaces to define partial functions on Type

Question

I'm trying to define something in Idris which would provide a way to represent types typographically. Think about Show, but instead of Showing elemenents of a type, I want to show the type itself. That would have the same practical effect of having defined a partial function on Type (that gives a type's representation) that a user could extend for their types as well.

My first idea, given the “user can extend functionality” requirement, was to use interfaces. So that would look something like this:

interface Representable a where
  representation : String

Some possible implementation would be

Representable Nat where
  representation = "Nat"

However, I come to a problem. Let's say I want to define a representation of the function type. That would be the representation of its domain, an arrow, and a representation of its range. So something like

(Representable a, Representable b) => Representable (a -> b) where
  representation = representation ++ " -> " ++ representation

The problem is now obvious. The compiler can't infer the representation's types on the right-hand side.

One alternative I came up with would be to create a Representation type that would carry an “artificial” argument:

data Representation : Type -> Type where
  Repr : (a : Type) -> String -> Representation a

Which would lead to

interface Representable a where
  representation : Representation a

And then

Representable Nat where
  representation = Repr Nat "Nat"

(Representable d, Representable r) => Representable (d -> r) where
  representation = Repr (d -> r) $
    (the (Representation d) representation)
    ++ " -> "
    ++ (the (Representation r) representation)

But then, off course, I get the error

Representations.idr:13:20-127:
   |
13 |   representation = Repr (d -> r) $ (the (Representation d) representation) ++ " -> " ++ (the (Representation r) representation)
   |                    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When checking right hand side of Representations.Representations.d -> r implementation of Representations.Representable, method representation with expected type
        Representation (d -> r)

When checking argument a to constructor Representations.Repr:
        No such variable d

However, I want representation to be argumentless – obviously, as it is a representation of the type, not its elements.

Does anyone have any sugestion on how to fix this particular error, or better yet, how to implement my idea in some not-so-horrifying-way?

Cactus Cactus · Accepted Answer · 2019-07-05T03:09:48

You can take an idea from Haskell and use a proxy to pass a token to representation with no term-level content:

data Proxy a = MkProxy

interface Representable a where
  representation : Proxy a -> String

Representable Nat where
  representation _ = "Nat"

(Representable a, Representable b) => Representable (a -> b) where
  representation {a = a} {b = b} _ = representation (MkProxy {a = a}) ++ " -> " ++ representation (MkProxy {a = b})

Using interfaces to define partial functions on Type

1 Answers