I realized that even the Newtype class only gets us to an approximation of the platonic ideal. In particular, my understanding is that n and n' are really supposed to be the same newtype, perhaps with different type arguments. Can we express that? I bet we can, with ConstraintKinds!
class (Sim n n', Sim n' n) => Similar n n'
instance (Sim n n', Sim n' n) => Similar n n'
type family GetArg (x :: j) :: k where
GetArg (_ a) = a
type family GetFun (x :: j) :: k where
GetArg (f _) = f
type family Sim (n :: k) (n' :: k) :: Constraint where
Sim (f a) n' = (Sim f (getFun n'), n' ~ getFun n' (GetArg n'))
Sim f g = f ~ g
I haven't tried compiling this, So I don't know if it works or even if it can be made to work, but I think it's a pretty interesting possibility.
I realized that even the
Newtype
class only gets us to an approximation of the platonic ideal. In particular, my understanding is thatn
andn'
are really supposed to be the same newtype, perhaps with different type arguments. Can we express that? I bet we can, withConstraintKinds
!I haven't tried compiling this, So I don't know if it works or even if it can be made to work, but I think it's a pretty interesting possibility.