Created
October 26, 2016 01:56
-
-
Save oliver-batchelor/e620fcdebbce82f2a0e0ae311c11ad31 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import Data.Type.Index | |
data Sum :: [Type] -> Type where | |
L :: x -> Sum (x : xs) | |
R :: Sum xs -> Sum (x : xs) | |
inj :: (Elem xs x) => x -> Sum xs | |
inj = inj' elemIndex | |
inj' :: Index xs x -> x -> Sum xs | |
inj' = \case | |
IZ -> L | |
IS x -> R . inj' x | |
class Proj x xs where | |
proj :: Proxy x -> Sum xs -> Maybe x | |
instance Proj x (x:xs) where | |
proj _ (L x) = Just x | |
proj _ _ = Nothing | |
instance Proj x ys => Proj x (y:ys) where | |
proj p (R ys) = proj p ys | |
data FList f xs where | |
FNil :: FList f '[] | |
(:<) :: Typeable x => f x -> FList f xs -> FList f (x : xs) | |
newtype Rev b a = Rev (a -> b) | |
elim :: FList (Rev a) xs -> Sum xs -> a | |
elim (Rev f :< fs) (L x) = f x | |
elim (_ :< fs) (R xs) = elim fs xs | |
infixr 5 :< | |
test, test1 :: Sum [Int, Double, Maybe String] | |
test = inj (3 :: Int) | |
test1 = inj (Just "fooobar") | |
f = (Rev show :< Rev show :< Rev show :< FNil) | |
res = (elim f test1, elim f test) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment