Using Quantified Constraints for Optics -- untypechecked (no compiler available)

QC.hs

{-# language TypeInType, QuantifiedConstraints, ConstraintKinds, RankNTypes, UndecidableInstances, MultiParamTypeClasses, TypeFamilies, KindSignatures #-}

module QC where

import Data.Constraint
import Data.Functor.Contravariant
import Data.Kind
import Data.Profunctor

type C = (Type -> Type) -> (Type -> Type -> Type) -> Constraint

class EqualityC p f
instance EqualityC p f

class (Profunctor p, Functor f) => IsoC p f
instance (Iso p, Functor f) => IsoC p f

class (Profunctor p, Applicative f) => PrismC p f
instance (Choice p, Applicative f) => PrismC p f

class (p ~ (->), Functor f) => LensC p f
instance (p ~ (->), Functor f) => LensC p f 

class (p ~ (->), Applicative f) => TraversalC p f
instance (p ~ (->), Applicative f) => TraversalC p f 

class (p ~ (->), Functor f, Contravariant f) => GetterC p f
instance (p ~ (->), Functor f, Contravariant f) => GetterC p f

class (p ~ (->), Applicative f, Contravariant f) => FoldC p f
instance (p ~ (->), Applicative f, Contravariant f) => FoldC p f

-- TODO: setters, indexed optics, etc.

type p ::- q = forall (a :: Type -> Type) (b :: Type -> Type -> Type). p a b :- q a b
type p =:> q = forall (a :: Type -> Type) (b :: Type -> Type -> Type). p a b => p a b

subs :: (p =:> q) => p ::- q
subs = Sub Dict

traversal_lens :: TraversalC ::- LensC
traversal_lens = subdicts

fold_traversal :: FoldC ::- TraversalC
fold_traversal = subdicts

prism_iso :: IsoC ::- PrismC
prism_iso = subdicts

type Opt c s t a b = forall p f. c p f => p a (f b) -> p s (f t)
type Opt' c s a = Opt c s s a a

type Lens = Opt LensC
type Lens' = Opt' LensC
type Traversal = Opt TraversalC
type Traversal' = Opt' TraversalC
type Prism = Opt PrismC
type Prism' = Opt' PrismC
type Iso = Opt IsoC
type Iso' = Opt' IsoC
type Equality = Opt EqualityC
type Equality = Opt' EqualityC
type Fold = Opt' FoldC
type Getter = Opt' FoldC

newtype Foo = Foo String deriving (Eq,Ord,Show,Read)

class (PrismC =:> AsFooC t) => AsFoo t where
  type AsFooC t :: C
  type AsFooC t = PrismC -- instances may optionally upgrade to IsoC or EqualityC
  _Foo :: Opt' (AsFooC t) t Foo

instance AsFoo Foo where
  type FooC Foo = EqualityC -- instances can tighten constraints
  _Foo = id

data Bar = FooCase !Foo | OtherCase !Int

makePrisms ''Bar

instance AsFoo Bar where
  _Foo = _FooCase

class (LensC =:> HasFooC t) => HasFoo t where
  type HasFooC t :: C
  type HasFooC t = LensC -- instances may add an index, upgrade to IsoC, EqualityC, etc.
  foo :: Opt' (HasFooC t) t Foo

instance HasFoo Foo where
  type HasFooC Foo = EqualityC
  foo = id

class (TraversalC =:> HasFoosC t) => HasFoos t where
  type HasFoosC t :: C
  type HasFoosC t = TraversalC -- instances may refine to LensC, PrismC, IsoC, EqualityC
  foos :: Opt' (HasFoosC t) t Foo

instance HasFoos Foo where
  type HasFoosC Foo = EqualityC
  foos = id