I stumbled across a tutorial on Idris, and after skimming through it, started reading up on "Dependent Types": http://en.wikipedia.org/wiki/Dependent_type
I can't see that there has been a discussion on how Nimrod relates to dependent types. I'm not an expert on type theory, so please excuse me if I get the terminology wrong here.
To me it seems that the array implementation in Nimrod really leads the language in this direction, and the first step has already been taken. In the development branch we now have static types, which allows any generic type to be dependent on a value.
The second step, it seems to me would be to allow the type system to evaluate simple expressions on values. For example, as far as I know there's no concatenate (&) operator on arrays, because that would require precisely this feature.
Let us for simplicity imagine arrays were defined on int (just their length), rather than a range. Then I imagine the implementation would look something like this:
template `&`[Ia, Ib,T](a: array[Ia: static[int], T], b: array[Ib: static[int], T]): array[Ia+Ib, T] =
for i in 0..(Ia-1):
result[i] = a[i]
for i in 0..(Ib-1):
result[Ia+i] = b[i]
Are there any plans for taking the language in this direction?
http://ceylon-lang.org/documentation/introduction/ lists it as "flow dependent typing" but indeed Google knows suprisingly little about it. Well the basic idea is that you give an expression a more specific type in some branches than in others:
proc takesRange(x: range[0..2]) = discard
var x = parseInt(readLine(stdin))
if x >= 0 and x <= 2:
# this compiles:
takesRange x
else:
# this does not:
takesRange x
Note that flow dependent typing is concerned with simple facts that can be extracted from the control flow graph and mostly deals with compile-time constants, whereas dependent typing is much more general.
(And yes I'm aware the example currently compiles either way and produces a runtime check instead.)
I agree with Araq, that the full scope of dependent typing seems too ambitious.
The flow-sensitive/dependent typing stuff seems quite exciting. Could it be generalized? Like say, if we can evaluate this procedure at compile-time, and it evaluates to true, then the type of the argument could be changed to so-and-so within that block. Anyway, it would be a very nice addition even if it was just for built-in types.
As for the example I went into, looking at the commit-history and some of the test-cases in devel, I think zah has been trying to make it possible to evaluate expressions on static types in the return type, there's one testcase that has the signature proc foo(a: static[string]): KK[a.len] for instance. But this area seems to be a minefield at the moment. I'm getting compiler crashes for a lot of the things I'm trying.
Excuse the necromancy, just wanted to share that the original & array concatenation works in current Nim, albeit not as a template.
func `&`[ia: static[int], ib: static[int], T](a: array[ia, T], b: array[ib, T]): array[ia + ib, T] =
for i in 0 ..< ia:
result[i] = a[i]
for i in 0 ..< ib:
result[ia + i] = b[i]
const a = [1, 2] & [3, 4] & [5, 6]
assert a.type is array[6, int]
assert a == [1, 2, 3, 4, 5, 6]
assert [1.0, 2.0] & [3.0, 4.0] is array[4, float]
assert [1.0, 2.0] & [3.0, 4.0] == [1.0, 2.0, 3.0, 4.0]