Hi there,
I'm new to Nim and I was experimenting with dependent types. I wanted to define arithmetic mod N in such a way that N is a type parameter.
I'll copy my code here:
type
Modulo[M: static[int]] = distinct int
proc `modulo`(v: int, M: static[int]): Modulo[M] = Modulo[M](v mod M)
proc `+`[M](m1, m2: Modulo[M]): Modulo[M] =
Modulo[M]((m1.int + m2.int) mod M)
#modulo(m1.int + m2.int, M)
proc `$`[M: static[int]](m: Modulo[M]): string =
$(m.int) & " mod " & $(M)
const
m = 10
let a = Modulo[m](1)
var b: Modulo[m] = modulo(11, m)
var c: Modulo[m] = modulo(a.int * b.int, m)
echo a
echo b
echo c
echo a + b
This is working, but I would like to use the constructor while defining +. If i comment the first line and decomment the second one in the + definition, something happens:
: too many arguments to function call, expected single argument 'v', have 2
arguments
result = modulo_90076((NI)(TMP141), ((NI) 10))
As you can see, modulo_90076 uses TMP141 (which is the addInt) and a constant term 10 (which is the value of m), but then it expects only one single argument, despite being defined with two arguments.
I am using nimrod version 0.11.2 (2015-06-02) on MacOSX: amd64, git hash 45b6082c1
I don't really know where to start about debugging this kind of error. Any help is appreciated!
Stefano