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•7h 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•11h ago
bgavran•7h 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