Is there any reason bidirectional pattern synonyms aren't in the library?

[dbeacham]

I couldn't find them in the library or any -extras package.

See post by @expipiplus1 in https://github.com/expipiplus1/vector-sized/issues/18#issuecomment-306854442 :

---

This is what I'm using. This allows one to construct vectors like:

test :: Vector 5 Int
test = 1 :> 2 :> 3 :> 4 :> 5 :> Nil

{-# LANGUAGE DataKinds       #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TypeOperators   #-}
{-# LANGUAGE ViewPatterns    #-}

module Data.Vector.Generic.Sized.Extra
  ( module V
  , pattern Nil
  , pattern (:>)
  , uncons
  ) where

import           Control.Arrow
import qualified Data.Vector.Generic.Base  as B
import           Data.Vector.Generic.Sized as V
import           GHC.TypeLits

pattern Nil :: B.Vector v a => Vector v 0 a
pattern Nil <- _
  where Nil = V.empty

infixr 5 :>
pattern (:>) :: B.Vector v a => a -> Vector v n a -> Vector v (1 + n) a
pattern h :> t <- (uncons -> (h, t))
  where (:>) = V.cons

uncons :: B.Vector v a => Vector v (1 + n) a -> (a, Vector v n a)
uncons = V.head &&& V.tail

Notation borrowed from https://hackage.haskell.org/package/clash-prelude-0.11.2/docs/CLaSH-Sized-Vector.html#t:Vec

[mstksg]

I think the main reason why this might have been withheld is that construction becomes basically O(n^2) this way, even though deconstruction isn't too bad. Offering this for construction, while convenient, would feel a bit misleading. People using cons-like patterns or constructors typically expect O(1), and they almost never want a version that is O(n). For small vectors this isn't a big deal, probably, but I feel like it's not the behavior people would actually want, and might surprise people/break expectations in ways they wouldn't realize until much later.

For deconstruction, at least, this pattern might be useful, non-misleading, unsurprising, so I don't see any reason why the deconstruction part wouldn't be good standalone.

For the construction of small vectors, we have fromTuple, so you can write

test :: Vector 5 Int
test = fromTuple (1,2,3,4,5)

and fromTuple is at least O(n), unlike the O(n^2) chained cons method.

If you want the consing syntax, you could even do:

test :: Vector 5 Int
Just test = fromList $ 1 : 2 : 3 : 4 : 5 : []

So I think it would be great to add at least the deconstruction direction of :>, but I'm suspicious about the construction direction...simply because you should never actually use it. Maybe adding it in with a big warning like WARNING: literally don't ever use this, there is usually either a better alternative or it doesn't do what you think wouldn't be so bad. But at that point, it feels more prudent to just not include the construction direction.

[expipiplus1]

Personally I'd be happy adding it for at least deconstruction, we might consider adding :< too perhaps (for snoc)...

For construction I wonder how many people would be using it without reading the documentation (and discovering @mstksg's warning).

[dbeacham]

I agree about construction - O(n^2) isn't really acceptable and will catch people out.

And the big win for me is to use it when passing vectors as function arguments

f :: Vector 2 Double -> Double
f (x :> y :> Nil) = x * y

[expipiplus1]

Cool,

If you open a PR with the unidirectional pattern synonym for all vector types I'd be happy to merge it.

On Wed, Dec 11, 2019, 7:45 PM David Beacham notifications@github.com wrote:

I agree about construction - O(n^2) isn't really acceptable and will catch people out.

And the big win for me is to use it when passing vectors as function arguments

f :: Vector 2 Double -> Double f (x :> y :> Nil) = x * y

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHub https://github.com/expipiplus1/vector-sized/issues/85?email_source=notifications&email_token=AAGRJXEJK23UO4KVBZ6AFBTQYDHGXA5CNFSM4JY7IS2KYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEGS2QXQ#issuecomment-564504670, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAGRJXHMFX24ZVFKXO45VMLQYDHGXANCNFSM4JY7IS2A .

[dbeacham]

Will do - any preferences for:

1. where it should live
2. if it should be re-exported from any other modules?

[kozross]

I think the correct answer for 1. is 'everywhere we define immutable vectors', as it applies equally to all of them, admittedly with different constraints. It also happens to be the answer for 2. The strategy I think best is to have the 'basic' pattern defined in the Data.Vector.Generic.Sized package, with a (Vector v a) constraint, and then 'specialized' versions exported from the more specialized packages (Data.Vector.Unboxed.Sized, Data.Vector.Storable.Sized, etc).

[mstksg]

I just realized that one thing we can do is try to actually have these patterns work like GADT patterns in which matching on Vector n a on each pattern reveals properties about the n. I wonder if this is possible or worth it ... or if it should be separated out

theThing :: KnownNat n => Vector n a -> String
theThing Empty = "empty"
theThing (_ :|> xs) = "not empty and " ++ show (V.length xs)

Hm, but if we do try to do this, it might make the COMPLETE pragmas less useful, and so just normal things like x :|> y :|> Empty would not be verifiable as COMPLETE, maybe. Maybe for now just this normal patch is ok and we can look into this second thing later.

[Bodigrim]

I think that construction is already covered by fromTuple. Is it considered unsatisfactory?

[expipiplus1]

Closed by fromTuple and https://github.com/expipiplus1/vector-sized/pull/88