An adjunction(?)

[masaeedu]

Hello there. So here's a neat little thing that possibly demonstrates Dict being one half of an adjunction between the Heyting algebra of constraints and the CCC of types and functions we know and love:

data a :- b
  where
  Proof :: (a ⇒ b) => a :- b
infixr 0 :-

instance Category (:-)
  where
  id = Proof
  Proof . Proof = Proof

-- A functor Constraint -> Type
type Dict :: Constraint -> Type
data Dict c
  where
  Dict :: c => Dict c

-- A functor Type -> Constraint
type Only :: Type -> Constraint
class Only x
  where
  only :: x

instance c => Only (Dict c)
  where
  only = Dict

type M c = Only (Dict c)
type C x = Dict (Only x)

-- The unit of the adjunction
unit :: c :- M c
unit = Proof

-- The counit of the adjunction
counit :: C x -> x
counit Dict = only

I don't have a lot of time to explore this further but I figured I'd dump the beginning of the idea here and someone can tear it apart if it's wrong/build on it if it makes sense.