Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- data Skolem (s :: Nat) = forall a. Skolem a
- unsafeUnskolem :: Skolem n -> a
- unsafeUnskolem (Skolem a) = unsafeCoerce a
- data Error e (m :: * -> *) a
- = Throw e
- | forall x. Catch (m x) (e -> m x) (x -> a)
- instance Functor m => Generic (Error e m a) where
- type Rep (Error e m a)
- = D1
- ('MetaData "Error" "TRYAGAIN" "main" 'False)
- (C1
- ('MetaCons "Throw" 'PrefixI 'False)
- (S1
- ('MetaSel
- 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
- (Rec0 e))
- :+: C1
- ('MetaCons "Catch" 'PrefixI 'False)
- (S1
- ('MetaSel
- 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
- (Rec0 (m (Skolem 0))
- :*: (S1
- ('MetaSel
- 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
- (Rec0 (e -> m (Skolem 0)))
- :*: S1
- ('MetaSel
- 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
- (Rec0 (Skolem 0 -> a))))))
- from (Throw e) = M1 $ L1 $ M1 $ M1 $ K1 $ e
- from (Catch a b c) =
- M1 $ R1 $ M1 $ M1 $ K1 (fmap Skolem a)
- :*: M1 (K1 $ \e -> fmap Skolem $ b e)
- :*: M1 (K1 $ \(Skolem s) -> c $ unsafeCoerce s)
- to (M1 (L1 (M1 (M1 (K1 e))))) = Throw e
- to (M1 (R1 (M1 (M1 (K1 a :*: (M1 (K1 b)) :*: (M1 (K1 c))))))) =
- Catch (fmap unsafeUnskolem a)
- (fmap (fmap unsafeUnskolem) b)
- (c . unsafeUnskolem)
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement