I could be jumping to an incorrect conclusion, but I think you are misreading the description of Ko's genericity. It doesn't mean that inputs and outputs are not distinguished. It just means that arguments and return values aren't explicitly typed. The kind of Prolog-style unification you are talking about is something different.