Types that constrain vectors based on norm

Question

In a language like Haskell or Idris, is it possible to create a data type which checks if an input vector for a function is, for instance, unitary? That is, can I create a data type SumsToOne which checks if a vector adds up to 1, etc?

Answer 1

Yes. In Idris it's kind of just as you say. You could wrap a list with a proof the elements sum to one

data SumsToOne : Type where
  STO : (xs : List Int) -> {auto prf : sum xs = 1} -> SumsToOne

Though if by data type you are referring to the proof, rather than the elements as well, you can just

go : (xs : List Int) -> {auto prf : sum xs = 1} -> <whatever you're returning>

The proof is of type sums xs = 1. prf is just the function parameter name, and auto means Idris will find the proof for you if it can.

I don't know if this will work for floating point elements.