Search code examples
constantsidrisdependent-typeparametric-polymorphism

Polymorphic constant in a dependent type signature?

Say I'd like to define a type of a proof that some vector has a certain sum. I'd also like that proof to work for any Monoid type t. My first attempt was this:

data HasSum : Monoid t => t -> Vect n t -> Type where
    EndNeutral : Monoid t => HasSum Prelude.Algebra.neutral []
    Component : Monoid t => (x : t) -> HasSum sum xs -> HasSum (x <+> sum) (x :: xs)

Unfortunately, the compiler argues it Can't find implementation for Monoid t. So I tried with an implicit argument so that I can specify its type:

    EndNeutral : Monoid t => {Prelude.Algebra.neutral : t} -> HasSum Prelude.Algebra.neutral []

This compiles, but this does not:

x : HasSum 0 []
x = EndNeutral

strangely claiming that it Can't find implementation for Monoid Integer.

My final attempt was to define a helper constant with capital letter name so that Idris doesn't confuse it for a bound variable:

ZERO : Monoid t => t
ZERO = neutral

data HasSum : Monoid t => t -> Vect n t -> Type where
    EndNeutral : Monoid t => HasSum ZERO []
    Component : Monoid t => {rem : t} -> (x : t) -> HasSum rem xs -> HasSum (x <+> rem) (x :: xs)

but now it can't guess the type of ZERO in the definition of EndNeutral (Can't find implementation for Monoid t). So I tried again with an implicit binding:

    EndNeutral : Monoid t => {ZERO : t} -> HasSum ZERO []

but now ZERO becomes a bound variable and although it compiles, it does not work as expected, because it allows to construct a proof of empty vectory having an arbitrary sum.

At this point I ran out of ideas. Does anyone know how to express a polymorphic constant in an Idris type?

Solution

  • It seems I found an answer finally. It might not be the best one, but it's the only one I'm aware of right now. So it is required to explicitly specify the type of neutral without adding an implicit argument (which would turn neutral into a bound variable). Of course, the function the can serve that purpose:

    data HasSum : Monoid t => t -> Vect n t -> Type where
    EndNeutral : Monoid t => HasSum (the t Prelude.Algebra.neutral) []
    Component : Monoid t => {rem : t} -> (x : t) -> HasSum rem xs -> HasSum (x <+> rem) (x :: xs)

    edit:

    A look at the type of neutral suggests yet another solution:

    > :doc neutral
Prelude.Algebra.neutral : Monoid ty => ty

    It appears the concrete type of neutral is in fact an implicit argument to it. Therefore:

    EndNeutral : Monoid t => HasSum (Prelude.Algebra.neutral {ty = t}) []

    also works.