3 ms·
Arithmetic inside the types not necessarily introduces undecidability. One example is telescopes for indices: data N where Z :: N O :: N -> N data
by thesz 1y ago
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 1y agoIndeed, 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. https://github.com/bgavran/TypeSafe_Tensors https://github.com/bgavran/TypeSafe_Tensors