@hache types can depend on other types
there are probably more rigorous definitions
i just noticed some patterns I've first seen in Agda so I wonder if it really has similar capabilities or if it's more like what Haskell has
@hache
in case that's still too vague, here is a basic example in Idris:
data List : (elem : Type) -> Type where
Nil : List elem
(::) : (x : elem) -> (xs : List elem) -> List elem
which is the typed linked list
@grainloom @hache This is not a dependent type, it is just parametric polymorphism which is much weaker. An example of a dependent type in Coq:
Inductive isEven : nat -> Type :=
| evenO : isEven 0
| evenSS n : isEven n -> isEven (S (S n)).
This type is constructed so that isEven n is inhabited iff n is even.
mmmm, it looks more like just generics, not proper dependent types with type level computations and stuff
CORRECTION
no it's not actually dependently typed, in case that wasn't clear
its creator even addresses that question and answers it with "I don't understand that stuff" so, nope, it's not depedent types, it just looked a lot like some of the simpler examples I've seen but it's just "parametric polymorphism" (or as i call it: "generics or something")
@grainloom What does "dependently typed" mean?