|
| 1 | +{-# OPTIONS_HADDOCK not-home #-} |
| 2 | + |
| 3 | +{-# LANGUAGE AllowAmbiguousTypes #-} |
| 4 | +{-# LANGUAGE ConstraintKinds #-} |
| 5 | +{-# LANGUAGE FlexibleContexts #-} |
| 6 | +{-# LANGUAGE FlexibleInstances #-} |
| 7 | +{-# LANGUAGE MultiParamTypeClasses #-} |
| 8 | +{-# LANGUAGE RankNTypes #-} |
| 9 | +{-# LANGUAGE ScopedTypeVariables #-} |
| 10 | +{-# LANGUAGE TypeApplications #-} |
| 11 | +{-# LANGUAGE TypeFamilies #-} |
| 12 | +{-# LANGUAGE TypeInType #-} |
| 13 | +{-# LANGUAGE TypeOperators #-} |
| 14 | +{-# LANGUAGE UndecidableInstances #-} |
| 15 | + |
| 16 | +{-| |
| 17 | +Module : OneOf.Fold |
| 18 | +Description : Functions for working with a 'OneOf' value. |
| 19 | +Copyright : (c) Tom Harding, 2018 |
| 20 | +License : MIT |
| 21 | + |
| 22 | +Stability : experimental |
| 23 | +
|
| 24 | +Given a @OneOf '[x, y, z]@, there are two sensible ways to interpret this: |
| 25 | +
|
| 26 | +- If everything in its list – @[x, y, z]@ – satisfy some constraint @c@, and we |
| 27 | + can write some @∀x. c x => x -> r@, then we can call this function on the |
| 28 | + value, regardless of its position, and produce some result. |
| 29 | +
|
| 30 | +- Instead of using implementations of a typeclass, we can produce a fold, |
| 31 | + taking functions to work with each of the possible branches. |
| 32 | +
|
| 33 | +There are trade-offs with both. The first method leads to much neater code, as |
| 34 | +we can simply write `interpret f xs` and get our "value" from inside. With the |
| 35 | +latter, however, we'll save on boilerplate in cases where we would potentially |
| 36 | +like many interpretations of the same value. The choice is yours. |
| 37 | +-} |
| 38 | +module OneOf.Fold where |
| 39 | + |
| 40 | +import Data.Kind (Constraint, Type) |
| 41 | +import OneOf.Types (OneOf(..)) |
| 42 | + |
| 43 | +-- | Interpret a @OneOf xs@ value, using knowledge that every member of @xs@ |
| 44 | +-- satisfies the given constraint, @c@. |
| 45 | + |
| 46 | +class Interpret (c :: Type -> Constraint) (xs :: [Type]) where |
| 47 | + |
| 48 | + -- | The usual rank-2 trick: "give me a function that relies on @c@'s |
| 49 | + -- interface to produce some value, and I'll produce that value". |
| 50 | + |
| 51 | + interpret :: (forall x. c x => x -> r) -> OneOf xs -> r |
| 52 | + |
| 53 | +instance c x => Interpret c '[x] where |
| 54 | + |
| 55 | + -- | Interpret a singleton list. Nothing especially clever: we know by |
| 56 | + -- construction that we must be looking at the type that is actually inside |
| 57 | + -- the 'OneOf', so we can just call the function on it. |
| 58 | + |
| 59 | + interpret f (Here x) = f x |
| 60 | + interpret _ (There _) = error "Impossible" |
| 61 | + |
| 62 | +instance (tail ~ (x' ': xs), Interpret c tail, c x) |
| 63 | + => Interpret c (x ': x' ': xs) where |
| 64 | + |
| 65 | + -- | For a non-singleton list (empty lists are impossible within 'OneOf'), we |
| 66 | + -- pattern match on whether we've found it or not. If we have, we do as we |
| 67 | + -- did above with the singleton. If we don't, we recurse deeper into the |
| 68 | + -- 'OneOf'. |
| 69 | + -- |
| 70 | + -- Note that we can avoid an overlapping instance by pattern-matching @tail@ |
| 71 | + -- a @Cons@ deeper. |
| 72 | + |
| 73 | + interpret f (Here x ) = f x |
| 74 | + interpret f (There x) = interpret @c f x |
| 75 | + |
| 76 | +-- | A @OneOf '[x, y]@ can be folded with @(x -> r) -> (y -> r) -> r@ – we just |
| 77 | +-- take a function for each possible value, and then apply the one that is |
| 78 | +-- relevant. This type family produces the signature, given the list. |
| 79 | + |
| 80 | +type family FoldSignature (xs :: [Type]) r where |
| 81 | + -- More recursion: take the head, add its fold, recurse. |
| 82 | + FoldSignature (x ': xs) r = (x -> r) -> FoldSignature xs r |
| 83 | + |
| 84 | + -- If we have no inputs, here's our output! |
| 85 | + FoldSignature '[] r = r |
| 86 | + |
| 87 | +-- | This type class builds the fold for a given 'OneOf' value. Once that has |
| 88 | +-- happened, usage is straightforward: |
| 89 | +-- |
| 90 | +-- > fold (inject True :: OneOf '[Int, String, Bool]) |
| 91 | +-- > (\_ -> "Int!") |
| 92 | +-- > (\case |
| 93 | +-- > "hello" -> "String!" |
| 94 | +-- > _ -> "Rude string :(") |
| 95 | +-- > (\x -> if x then "YAY" else "BOO") |
| 96 | +-- |
| 97 | +-- We can now fold out of our datatype just as we would with @either@. |
| 98 | + |
| 99 | +class BuildFold xs result where |
| 100 | + |
| 101 | + -- | Fold a 'OneOf' value by providing a function for each possible type. |
| 102 | + -- |
| 103 | + -- >>> :t fold (undefined :: OneOf '[a, b]) |
| 104 | + -- fold (undefined :: OneOf '[a, b]) |
| 105 | + -- :: (a -> result) -> (b -> result) -> result |
| 106 | + |
| 107 | + fold :: OneOf xs -> FoldSignature xs result |
| 108 | + |
| 109 | +instance BuildFold '[x] result where |
| 110 | + |
| 111 | + -- | For a singleton list (again, empties are impossible), we needn't do |
| 112 | + -- anything too clever: we just apply the function to the head. |
| 113 | + |
| 114 | + fold (Here x) f = f x |
| 115 | + fold (There _) _ = error "Impossible" |
| 116 | + |
| 117 | +instance (tail ~ (x' ': xs), BuildFold tail result, Ignore tail result) |
| 118 | + => BuildFold (x ': x' ': xs) result where |
| 119 | + |
| 120 | + -- | Things get more tricky for a non-singleton list if you find a match; how |
| 121 | + -- do you pass it over all the arguments in your fold? |
| 122 | + -- |
| 123 | + -- Again, we avoid an overlapping instance by matching @tail@ as a @Cons@. |
| 124 | + |
| 125 | + fold (There x) _ = fold @_ @result x |
| 126 | + fold (Here x) f = ignore @tail (f x) |
| 127 | + |
| 128 | +class Ignore (args :: [Type]) result where |
| 129 | + |
| 130 | + -- | @Ignore@ is a class whose only purpose is to generate n-ary @const@ |
| 131 | + -- functions. Give it a result, and it'll figure out the type of a function |
| 132 | + -- that ignores all its arguments. |
| 133 | + |
| 134 | + ignore :: result -> FoldSignature args result |
| 135 | + |
| 136 | +-- | An empty list of arguments means we're ready to return the result! |
| 137 | +instance Ignore '[] result where |
| 138 | + ignore result = result |
| 139 | + |
| 140 | +instance Ignore xs result |
| 141 | + => Ignore (x ': xs) result where |
| 142 | + |
| 143 | + -- | Provided I can ignore the tail, I can remove the whole thing. How? I |
| 144 | + -- just insert another argument and ignore that as well! |
| 145 | + |
| 146 | + ignore result _ = ignore @xs result |
0 commit comments