blob: 738017500d8b23e6885b1956a5269d7d51e11cf2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
|
{-# LANGUAGE ScopedTypeVariables, PatternSynonyms, DataKinds, PolyKinds,
GADTs, TypeOperators, TypeFamilies #-}
module T13441 where
import Data.Functor.Identity
data FList f xs where
FNil :: FList f '[]
(:@) :: f x -> FList f xs -> FList f (x ': xs)
data Nat = Zero | Succ Nat
type family Length (xs :: [k]) :: Nat where
Length '[] = Zero
Length (_ ': xs) = Succ (Length xs)
type family Replicate (n :: Nat) (x :: a) = (r :: [a]) where
Replicate Zero _ = '[]
Replicate (Succ n) x = x ': Replicate n x
type Vec n a = FList Identity (Replicate n a)
-- Using explicitly-bidirectional pattern
pattern (:>) :: forall n a. n ~ Length (Replicate n a)
=> forall m. n ~ Succ m
=> a -> Vec m a -> Vec n a
pattern x :> xs <- Identity x :@ xs
where
x :> xs = Identity x :@ xs
-- Using implicitly-bidirectional pattern
pattern (:>>) :: forall n a. n ~ Length (Replicate n a)
=> forall m. n ~ Succ m
=> a -> Vec m a -> Vec n a
pattern x :>> xs = Identity x :@ xs
|
