Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- module Main where
- -- We will define our checker by piecing together functions based on the various types of binders.
- -- We use prisms to abstract over the data constructors representing binders
- type Prism a b = (a -> b, b -> Maybe a)
- -- As an example, suppose we want to check array binders [_, _, ..., _] for exhaustivity.
- -- We could introduce two constructors ArrNil and ArrCons, and require these constructors be
- -- binders in our language.
- data Array b = ArrNil | ArrCons b b deriving (Show)
- -- Here, I'm just implementing the "complement" function, which generates all
- -- patterns uncovered by a given pattern. This function lifts such a function to
- -- handle array binders.
- missArray :: Prism Wildcard b -> Prism (Array b) b -> (b -> [b]) -> b -> [b]
- missArray (wild, _) (inj, prj) f b =
- case prj b of
- Just arr -> go arr
- Nothing -> f b
- where
- go ArrNil = [inj (ArrCons (wild Wildcard) (wild Wildcard))]
- go (ArrCons x xs) = inj ArrNil : map (inj . (`ArrCons` xs)) (f x) ++ map (inj . ArrCons x) (f xs)
- -- We can handle wildcards similarly
- data Wildcard = Wildcard
- missWildcard :: Prism Wildcard b -> (b -> [b]) -> b -> [b]
- missWildcard (_, prj) f b =
- case prj b of
- Just _ -> []
- Nothing -> f b
- -- Now we can assemble our complement function piece-by-piece by specifying a few prisms.
- data Test = Wild | Arr (Array Test) deriving (Show)
- test = missArray wildPrism arrPrism
- . missWildcard wildPrism
- $ test
- arrPrism = (Arr, isArr)
- where
- isArr (Arr a) = Just a
- isArr _ = Nothing
- wildPrism = (const Wild, isWild)
- where
- isWild Wild = Just Wildcard
- isWild _ = Nothing
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement