Comment puis-je combiner cette famille de type fermé avec une classe de type dépendant ?

Question

Mon problème

J'ai la famille de type suivante qui sépare les arguments d'une fonction :

type family
  SeparateArgs
    ( a :: Type )
      :: ( Type, [Type] )
  where
    SeparateArgs (a -> b) =
      SndCons2 a (SeparateArgs b)
    SeparateArgs a =
      '(a, '[])

J'ai aussi cette classe de type pour faire l'inverse :

class Refunct args goal newSig | args goal -> newSig where
  refunct :: (HList args -> goal) -> newSig
instance Refunct '[] goal goal where
  refunct makeA = makeA HNil
instance
  ( Refunct tailArgs goal c
  )
    => Refunct (headArg ': tailArgs) goal (headArg -> c)
  where
    refunct hFunct x = refunct $ hFunct . (x :>)

Maintenant, à peu près chaque fois que j'utilise ces deux-là, je les utilise ensemble comme suit :

instance
  ( SeparateArgs a ~ '(goal, args)
  , Refunct goal args a
  , ...
  )
    => ...

Ainsi, je peux séparer les arguments, effectuer un traitement pour créer une fonction du type HList args -> goal et ensuite le transformer en une fonction régulière.

Cela fonctionne mais c'est assez frustrant car je sais que Separate a ~ '(goal, args) => Refunct args goal a ce qui signifie qu'une seule de ces déclarations est nécessaire. Cependant, le compilateur ne peut pas le savoir et je dois donc l'en informer.

Ce n'est bien sûr pas critique, puisque mon code fonctionne actuellement, mais je voudrais le regrouper en une seule déclaration. Idéalement en ajoutant une seconde dépendance fonctionnelle à Refunct comme ça :

class
  ( SeparateArgs newSig ~ '(goal, args)
  )
    => Refunct args goal newSig
  | args goal -> newSig
  , newSig -> args goal
  where
    refunct :: (HList args -> goal) -> newSig

(Bien sûr, cela ne fonctionne pas tout seul).

Existe-t-il un moyen de réduire les deux (la famille de type SeparateArgs et la classe de type Refunct ) en une seule contrainte ? Je suis toujours prêt à définir des constructions supplémentaires, je voudrais simplement avoir des contraintes non redondantes dans le résultat. J'aurai toujours besoin de la refunct fonction.

Si cela est nécessaire, voici mon implémentation de HList :

data HList (a :: [ Type ]) where
  HNil :: HList '[]
  (:>) :: a -> HList b -> HList (a ': b)

hHead :: HList (a ': b) -> a
hHead (a :> _) = a

hTail :: HList (a ': b) -> HList b
hTail (_ :> b) = b

Ce que j'ai essayé

Après en avoir discuté ailleurs, il m'a été suggéré d'essayer :

type family
  IsAtomic
    ( a :: Type )
      :: Bool
  where
    IsAtomic (a -> b) = 'False
    IsAtomic a = 'True

class
  Refunct args goal newSig
  | args goal -> newSig
  , newSig -> args goal
  where
    refunct :: (HList args -> goal) -> newSig
instance
  ( IsAtomic goal ~ 'True
  )
    =>  Refunct '[] goal goal
  where
  refunct makeA = makeA HNil
instance
  ( Refunct tailArgs goal c
  , IsAtomic (headArg -> c) ~ 'False
  )
    => Refunct (headArg ': tailArgs) goal (headArg -> c)
  where
    refunct hFunct x = refunct $ hFunct . (x :>)

Nous ajoutons ici une contrainte supplémentaire selon laquelle la première instance ne fonctionne que si IsAtomic goal ~ 'True et le second seulement si IsAtomic goal ~ 'False donde IsAtomic est une famille de type que j'ai défini qui est 'False sur les fonctions et 'True sur tout le reste.

Ici, le compilateur semble incapable de confirmer que les deux instances ne violent pas la dépendance fonctionnelle. L'erreur exacte est la suivante :

    Functional dependencies conflict between instance declarations:
      instance (IsAtomic goal ~ 'True) => Refunct '[] goal goal
      instance (Refunct tailArgs goal c, IsAtomic goal ~ 'False) =>
               Refunct (headArg : tailArgs) goal (headArg -> c)
    |
XXX |   ( IsAtomic goal ~ 'True
    |   ^^^^^^^^^^^^^^^^^^^^^^^...

(ok ce n'est pas exact puisque j'ai enlevé toutes les informations d'identification).

Mon intuition ici est qu'il n'est pas conscient que IsAtomic goal ~ 'True y IsAtomic goal ~ 'False ne peuvent pas être toutes deux vraies en même temps. C'est raisonnable puisque sans inspection, nous ne pouvons pas savoir IsAtomic n'est pas forall a. a qui satisfait les deux contraintes.

Answer 1

Que voulons-nous ?

Pour résoudre ce problème, nous devons d'abord déterminer ce que nous voulons.

Nous voulons que le comportement d'une famille de types fermée (de sorte que les fonctions et les non-fonctions correspondent à des instances différentes) mais nous voulons également construire des données comme une classe de types (de sorte que nous pouvons obtenir refunct ).

C'est-à-dire que nous voulons une classe de type avec la logique d'une famille de type proche. Pour cela, il suffit de séparer les deux parties et de les implémenter séparément : la logique comme une famille de types fermée et le reste comme une classe de types.

Maintenant, pour faire cela, nous prenons notre famille de type et nous ajoutons un autre paramètre.

class
  Foo
    (bar :: Type)
    (baz :: Type)
    (bax :: Type)

devient

class
  Foo'
    (flag :: Flag)
    (bar :: Type)
    (baz :: Type)
    (bax :: Type)

Ce paramètre agira comme un drapeau pour nous indiquer quelle instance utiliser. Puisqu'il est du type Flag nous devons faire ce type de données. Il doit avoir un constructeur pour chaque instance (nous pouvons être un peu plus souples avec cela dans certains cas, mais en général, vous voudriez un à un).

data Flag = Instance1 | Instance2 | Instance3 ...

(Dans le cas de mon problème, étant donné qu'il n'y a que deux instances nous utilisons Bool )

Maintenant, nous construisons une famille de types fermée qui calcule quelle instance correspond. Elle doit prendre les arguments pertinents dans les paramètres de Foo et produire un Flag

type family
  FooInstance
    (bar :: Type)
    (baz :: Type)
    (bax :: Type)
      :: Flag
  where
    FooInstance ... = Instance1
    FooInstance ... = Instance2
    FooInstance ... = Instance3
    ...

Dans le cas de la question qui nous occupe, nous appelons cela IsAtomic puisque ce nom est descriptif de ce qu'il fait.

Maintenant, nous modifions nos instances pour qu'elles correspondent à la bonne Flag s. C'est assez simple, il suffit d'ajouter le drapeau d'instance à la déclaration :

instance
  ( Foo newBar newBaz newBax
  ...
  )
    => Foo' 'Instance3 foo bar baz bax
  where
    ...

Il est important de noter que nous no changer les appels récursifs à Foo à des appels à Foo' . Nous sommes sur le point de construire Foo comme une enveloppe autour de Foo' qui gère notre famille de types fermés ( FooInstance dans ce cas), nous voulons donc appeler la fonction Foo pour éviter d'invoquer la même logique à chaque fois.

C'est construit comme ça :

class
  Foo
    (bar :: Type)
    (baz :: Type)
    (bax :: Type)
  where
    ...
instance
  ( Foo' (FooInstance bar baz bax) bar baz bax
  )
    => Foo bar baz bax
  where
    ...

Si nous voulons être encore plus sûrs, nous pouvons ajouter une ligne à chacun des éléments suivants Foo' pour vérifier qu'elle est appelée correctement :

instance
  ( Foo newBar newBaz newBax
  , FooInstance bar baz baz ~ 'Instance3
  ...
  )
    => Foo' 'Instance3 bar baz bax
  where
    ...

Ma solution

Nous utilisons donc maintenant cette stratégie pour la question spécifique qui nous occupe. Voici le code dans son intégralité. La classe concernée est SeparateArgs :

type family
  IsAtomic
    ( a :: Type )
      :: Bool
  where
    IsAtomic (a -> b) = 'False
    IsAtomic a = 'True

class
  SeparateArgs
    (args :: [Type])
    (goal :: Type)
    (newSig :: Type)
  | args goal -> newSig
  , newSig -> args goal
  where
    refunct :: (HList args -> goal) -> newSig

instance
  ( IsAtomic newSig ~ isAtomic -- For (possible? compilation time) speedup
  , SeparateArgs' isAtomic args goal newSig
  )
    => SeparateArgs args goal newSig
  where
    refunct = refunct' @isAtomic

class
  SeparateArgs'
    (isAtomic :: Bool)
    (args :: [Type])
    (goal :: Type)
    (newSig :: Type)
  | args goal -> newSig isAtomic
  , newSig isAtomic -> args goal
  where
    refunct' :: (HList args -> goal) -> newSig
instance
  ( IsAtomic goal ~ 'True -- Only exists to ensure we are not invoking this in an illegal manner
  )
    => SeparateArgs' 'True '[] goal goal
  where
    refunct' makeA = makeA HNil
instance
  ( IsAtomic (headArg -> c) ~ 'False -- Only exists to ensure we are not invoking this in an illegal manner
  , SeparateArgs tailArgs goal c
  )
    => SeparateArgs' 'False (headArg ': tailArgs) goal (headArg -> c)
  where
    refunct' hFunct x = refunct $ hFunct . (x :>)