Closed chessai closed 5 years ago
Lots of functions in this module are not total. I plan to use refined to make them total.
refined
Another thing, the Matrix types are totally unsafe. Basically, I think Matrix should look like this:
Matrix
data Matrix :: Nat -> Nat -> Type -> Type where Matrix :: !(Vector (C a)) -> a
C is a closed injective type family that maps Haskell types to their C counterparts. In other words,
C
a ~ Complex ===> C a ~ CComplex, etc.
a ~ Complex ===> C a ~ CComplex
Lots of functions in this module are not total. I plan to use
refinedto make them total.Another thing, the Matrix types are totally unsafe. Basically, I think
Matrixshould look like this:data Matrix :: Nat -> Nat -> Type -> Type where Matrix :: !(Vector (C a)) -> a
Cis a closed injective type family that maps Haskell types to their C counterparts. In other words,a ~ Complex ===> C a ~ CComplex, etc.