Skip to content

Instantly share code, notes, and snippets.

@edwardgeorge

edwardgeorge/forall-entailment.hs

Created June 5, 2017 08:39
Show Gist options
  • Save edwardgeorge/5aa08a73bdee02843f5cabc72989e6c9 to your computer and use it in GitHub Desktop.
Save edwardgeorge/5aa08a73bdee02843f5cabc72989e6c9 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
forall-entailment.hs
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, TypeFamilies, ScopedTypeVariables, RankNTypes,
ConstraintKinds, TypeOperators, UndecidableInstances #-}
module Lib2 where
import Data.Constraint
import Data.Constraint.Forall
class C1 a b
class C2 a b
instance C1 a b => C2 a b
foo :: (forall a. Dict (c a) -> Dict (d a)) -> Forall c :- Forall d
foo f = baz (bar f)
bar :: forall c d. (forall a. Dict (c a) -> Dict (d a)) -> Dict (Forall c) -> Dict (Forall d)
bar f Dict = forall $ case inst :: Forall c :- c a
of Sub a -> f a
baz :: (Dict (Forall c) -> Dict (Forall d)) -> Forall c :- Forall d
baz f = Sub $ f Dict
impl :: Forall (C1 a) :- Forall (C2 a)
impl = foo $ \Dict -> Dict
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment