Specialization in compile time

[dumblob]

Can I somehow express in Kind, that applying sort() on a list of strings shall use a generic sorting algorithm, but applying the same sort() function to a list of integers shall use e.g. radix sort?

[rigille]

so if I understand correctly you would like to define a function List.sort<A: Type>(xs: List<A>): List<A> so that calling List.sort<String>(xs) uses an algorithm but calling List.sort<Int>(xs) uses another, choosing the most efficient algorithm automatically without the user needing to think about it. is that correct?
that isn't possible because kind doesn't support type cases. however you could do something similar:
first define the subset of Types your function will support with an indexed type.

type SortType ~ (A: Type) {
  int ~ (A = Int)
  str ~ (A = String)
}

you can think of those elements as evidence of membership in the subset your defined. if you have that then you can define your sorting function like this

List.sort<A: Type>(Ev: SortType(A), xs: List<A>): List<A>
  case Ev {
    int: ?radix_sort
    str: ?generic_sort
  }

doing case analysis on the evidence. and you can call it like this

xs = [+1, -2, +3]
ys = ["a", "aa", "aaa"]
List.sort!!(xs)
List.sort!!(ys)

because kind should be able to fill those holes. however trying this

zs = [1, 2, 3] :: List<Nat>
List.sort!!(zs)

shouldn't ever typecheck because there's no evidence for SortType(Nat).

as of kind 1.0.32 the typechecker isn't filling those holes correctly, that's a bug and will be fixed.

[dumblob]

Thanks for a detailed answer! I think this principle is acceptable (at least for now).

Should the need for "compile time specialization" become stronger (e.g. with the advent of optimization phase of the Kind compiler development), this might be reconsidered (from syntactic sugar to the compiler giving some advices to users based on frequent patterns).

Shall we leave this open and tag it as something related e.g. to optimization?

[VictorTaelin]

Kind doesn't actually create new constructors when filling holes. That'd step on the realms of unification, which we avoid to keep the type-checker simpler and faster. Perhaps in a future?