Structuring Arrays with Algebraic Shapes [video]

2 comments

• thesz 3 days 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 3 days 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.

    https://github.com/bgavran/TypeSafe_Tensors