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.
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