Closed martijnbastiaan closed 7 months ago
Was there a reason you use :> instead of Cons for the pattern match?
Discussed in the office: there is a difference in behavior. E.g. in the following:
vecToTuplePat :: (Vec 2 a) -> (a, a)
vecToTuplePat (a1 :> a2 :> _) = (a1, a2)
-- True
pat :: Bool
pat = case vecToTuplePat (1 :> undefined) of
~(a, _) -> a `seq` True
vecToTupleCon :: (Vec 2 a) -> (a, a)
vecToTupleCon (a1 `Cons` a2 `Cons` _) = (a1, a2)
-- Bottom
con :: Bool
con = case vecToTupleCon (1 :> undefined) of
~(a, _) -> a `seq` True
then pat ~ True
, while con ~ _|_
. We're not sure whether this will be an issue in practice, but we've decided to err on the safe side and be lazy.
@leonschoorl I applied your suggestions, thanks!
Newer GHCs (mistakenly) emit warnings when pattern matching on
Vec
s, with neither:>
norCons
being able to prevent it.vecToTuple
allows users to convertVec
s to tuples, sidestepping GHCs exhaustiveness checker while not compromising on safety.Nested tuples were considered as an alternative implementation, simplifying implementation and removing the need for
TemplateHaskell
. This would, however, compromise on user comfort while offering no expected real-world benefits.This is clearly a work around. Perhaps we should write a GHC plugin to circumvent these warnings (and depending on the solution upstream)?
Documentation
Still TODO: