How can I (if it's possible) write
reifiedDimension
in Haskell?
Using GHC.TypeLits
and ScopedTypeVariables
:
instance SingI d => Applicative (Point d) where
pure = Point . Vector.replicate reifiedDimension
where reifiedDimension = fromInteger $ fromSing (sing :: Sing d)
...
See my answer here for a full example.
Moreover, again if possible, given
(Point v1) :: Point d1 a
and(Point v2) :: Point d2 a
how can I getlength v1 == length v2
can I getd1 ~ d2
?
With Data.Vector
, no. You'd need a vector type that encodes the length in the type. The best you can do is to maintain this yourself and encapsulate it by not exporting the Point
constructor.