Existe-t-il un moyen général d'appliquer des contraintes à une application de type?

Question

A comment par l'utilisateur 2426021684 m'a amené à étudier s'il était possible de trouver une fonction de type F telle que F c1 c2 fa démontre que pour certains f et a:

1. fa ~ f a
2. c1 f
3. c2 a

Il s'avère que le plus simple RM est assez facile. Cependant, j'ai trouvé qu'il était plutôt difficile de savoir comment écrire une version poly-aimée. Heureusement, j'ai réussi à trouver un moyen que j'écrivais cette question.

Answer 1

Tout d'abord, un peu passe-partout:

{-# LANGUAGE TypeFamilies #-} 
{-# LANGUAGE ConstraintKinds #-} 
{-# LANGUAGE FlexibleContexts #-} 
{-# LANGUAGE FlexibleInstances #-} 
{-# LANGUAGE MultiParamTypeClasses #-} 
{-# LANGUAGE UndecidableInstances, UndecidableSuperClasses #-} 
{-# LANGUAGE PolyKinds #-} 
{-# LANGUAGE TypeOperators #-} 
{-# LANGUAGE ScopedTypeVariables #-} 

module ConstrainApplications where 

import GHC.Exts (Constraint) 
import Data.Type.Equality 

Maintenant, tapez les familles à déconstruire des applications sur des types arbitraires.

type family GetFun a where 
    GetFun (f _) = f 
type family GetArg a where 
    GetArg (_ a) = a 

Maintenant, une fonction de type très générale, plus générale que nécessaire pour répondre à la question. Mais cela permet une contrainte impliquant les deux composants de l'application.

type G (cfa :: (j -> k) -> j -> Constraint) (fa :: k) 
    = (fa ~ (GetFun fa :: j -> k) (GetArg fa :: j) 
    , cfa (GetFun fa) (GetArg fa)) 

Je n'aime pas offrir des fonctions de contrainte sans classes pour correspondre, alors voici une version de première classe de G.

class G cfa fa => GC cfa fa 
instance G cfa fa => GC cfa fa 

Il est possible d'exprimer F en utilisant G et une classe auxiliaire:

class (cf f, ca a) => Q cf ca f a 
instance (cf f, ca a) => Q cf ca f a 

type F cf ca fa = G (Q cf ca) fa 

class F cf ca fa => FC cf ca fa 
instance F cf ca fa => FC cf ca fa 

Voici quelques exemple utilise des F:

t1 :: FC ((~) Maybe) Eq a => a -> a -> Bool 
t1 = (==) 

-- In this case, we deconstruct the type *twice*: 
-- we separate `a` into `e y`, and then separate 
-- `e` into `Either x`. 
t2 :: FC (FC ((~) Either) Show) Show a => a -> String 
t2 x = case x of Left p -> show p 
       Right p -> show p 

t3 :: FC Applicative Eq a => a -> a -> GetFun a Bool 
t3 x y = (==) <$> x <*> y