Arithmetic inside the types not necessarily introduces undecidability. One example is telescopes for indices:
data N where
Z :: N
O :: N -> N
data T (n :: N) where
TZ :: T (O n)
TO :: T n -> T (O n)
To safely access an element in array you have to provide a proof that a telescope can be constructed for given index range.
bgavran•6mo ago
Indeed, the author seems to have a misunderstanding about both undecidability and complexity as they pertain to dependent types.
Dependent types do not add complexity to our system, they reveal it.
Case in point: here is a fully dependently-typed tensor processing framework written in Idris, which I believe matches most of the desiderata of his talk, capturing even a generalisation of arrays via Naperian functors that is mentioned at one point.
thesz•6mo ago
bgavran•6mo ago
Dependent types do not add complexity to our system, they reveal it.
Case in point: here is a fully dependently-typed tensor processing framework written in Idris, which I believe matches most of the desiderata of his talk, capturing even a generalisation of arrays via Naperian functors that is mentioned at one point.
https://github.com/bgavran/TypeSafe_Tensors