Defining Function at Type-Level for Mod (%)?

[Kevin Meredith]

Is it possible, at the type level, i.e. at compile-time, to define a function:

onlyModBy5 : Nat -> Nat

that is, only accept a Nat argument that's evenly divisible by 5.

Example:

* compiles successfully *

onlyModBy5 5

onlyModBy5 10

onlyModBy5 25

...

* fails to compile *

onlyModBy5 6

onlyModBy5 11

onlyModBy5 12

...

If so, please give me a hint on how to do this.

Thanks

[David Raymond Christiansen]

Hi Kevin

One way to formulate "n is evenly divisible by 5" is "there is a number
k such that k * 5 = n". You could then do:

onlyModByFive : (n : Nat) -> (k : Nat ** 5 * k = n) -> Nat

But it really depends on why you want it only divisible by five, and
what sorts of automation you require. Take a look at the implementations
of divMod in the contrib package for more possibilities.

/David

> --
> You received this message because you are subscribed to the Google
> Groups "Idris Programming Language" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to idris-lang+...@googlegroups.com
> <mailto:idris-lang+...@googlegroups.com>.
> For more options, visit https://groups.google.com/d/optout.

[bo...@pik-potsdam.de]

Kevin,

the notion that a number is a divisor of another one is one that
deserves to be formalized, in my opinion. You could have a look at

https://github.com/nicolabotta/SeqDecProbs/blob/master/frameworks/14-/NatDivisor.lidr
https://github.com/nicolabotta/SeqDecProbs/blob/master/frameworks/14-/NatDivisorOperations.lidr
https://github.com/nicolabotta/SeqDecProbs/blob/master/frameworks/14-/NatDivisorProperties.lidr

With 'Divisor' in place, you could then just say something like

> onlyModBy5 : (n : Nat) -> 5 `Divisor` n -> Nat

Perhaps you could also try collecting those values that are divisible by
5 in a suitable interface, something like

> interface HasDivisor5 (n : Nat) where
> lala : (q : Nat ** 5 * q = n)

and then say something like

> onlyModBy5 : (HasDivisor5 n) => Nat

Ciao,
Nicola

> --
> You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.

> To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.

[Kevin Meredith]

Hi David -

Could you please explain:

* this syntax - (k : Nat ** 5 * k = n)

* why `n` is needed?

[Kevin Meredith]

Cactus provided another helpful answer - http://stackoverflow.com/a/36465477/409976.