Haskell/GHC :Comment écrire des prédicats sur les naturels au niveau du type

Question

J'aurais juré avoir vu un article à ce sujet récemment, mais je ne le trouve pas.

J'essaie de créer un type pour faire un encodage binaire du mod de nombres n, mais pour ce faire, je dois être capable d'écrire des prédicats au niveau du type naturals :

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
module Modulo where

-- (pseudo-)binary representation of 
-- numbers mod n
--
--  e.g. Mod Seven contains
--    Zero . Zero . Zero $ Stop
--    Zero . Zero . One  $ Stop
--    Zero . One . Zero $ Stop
--    Zero . One . One  $ Stop
--    One . Zero . Zero $ Stop
--    One . Zero . One  $ Stop
--    One . One $ Stop 
data Mod n where
  Stop :: Mod One
  Zero :: Split n => Mod (Lo n) -> Mod n
  One  :: Split n => Mod (Hi n) -> Mod n

-- type-level naturals
data One
data Succ n 
type Two = Succ One

-- predicate to allow us to compare 
-- natural numbers
class Compare n n' b | n n' -> b

-- type-level ordering
data LT
data EQ
data GT

-- base cases
instance Compare One One EQ
instance Compare One (Succ n) LT
instance Compare (Succ n) One GT

-- recurse
instance Compare n n' b => Compare (Succ n) (Succ n') b

-- predicate to allow us to break down
-- natural numbers by their bit structure
--
-- if every number mod n can be represented in m bits, then
class Split n where
  type Lo n -- number of values mod n where the m'th bit is 0
  type Hi n -- number of values mod n where the m'th bit is 1

-- base case, n = 2
-- for this, we only need m=1 bit
instance Split Two where
  type Lo Two = One -- 0 mod 2
  type Hi Two = One -- 1 mod 2

-- recurse
--  if (Lo n) == (Hi n), then n = 2^m, so
--  the values mod (n+1) will require one extra bit
instance (Split n, Compare (Lo n) (Hi n) EQ) => Split (Succ n) where
  type Lo (Succ n) = n    -- all the numbers mod n will be prefixed by a 0
  type Hi (Succ n) = One  -- and one extra, which will be 10...0

-- recurse
--  if (Lo n) > (Hi n), then n < 2^m, so
--  the values mod (n+1) still only require m bits
instance (Split n, Compare (Lo n) (Hi n) GT) => Split (Succ n) where
  type Lo (Succ n) = Lo (n)       -- we've got the same number of lower values
  type Hi (Succ n) = Succ (Hi n)  -- and one more higher value

Mon implémentation actuelle génère un tas d'erreurs de compilation :

Nat.hs:60:8:
    Conflicting family instance declarations:
      type Lo Two -- Defined at Nat.hs:60:8-9
      type Lo (Succ n) -- Defined at Nat.hs:74:8-9

Nat.hs:61:8:
    Conflicting family instance declarations:
      type Hi Two -- Defined at Nat.hs:61:8-9
      type Hi (Succ n) -- Defined at Nat.hs:75:8-9

Nat.hs:66:10:
    Duplicate instance declarations:
      instance (Split n, Compare (Lo n) (Hi n) EQ) => Split (Succ n)
        -- Defined at Nat.hs:66:10-62
      instance (Split n, Compare (Lo n) (Hi n) GT) => Split (Succ n)
        -- Defined at Nat.hs:73:10-62

Nat.hs:67:8:
    Conflicting family instance declarations:
      type Lo (Succ n) -- Defined at Nat.hs:67:8-9
      type Lo (Succ n) -- Defined at Nat.hs:74:8-9

Nat.hs:68:8:
    Conflicting family instance declarations:
      type Hi (Succ n) -- Defined at Nat.hs:68:8-9
      type Hi (Succ n) -- Defined at Nat.hs:75:8-9

Ce qui me fait penser que je vais mal écrire mes prédicats, s'il pense qu'ils sont en conflit.

Comment puis-je les faire correctement ?

Answer 1

Le problème du conflit est assez simple.Le règles pour les familles de types qui se chevauchent sont assez simples :

Les déclarations d'instance d'une famille de types utilisée dans un seul programme ne peuvent se chevaucher que si les côtés droits des instances qui se chevauchent coïncident pour les types qui se chevauchent.Plus formellement, deux déclarations d'instance se chevauchent s'il existe une substitution qui rend les côtés gauches des instances syntaxiquement identiques.Chaque fois que tel est le cas, les membres de droite des instances doivent également être syntaxiquement égaux sous la même substitution.

Notez qu'il précise syntaxiquement égal.Considérez ces deux cas :

instance Split Two where
  type Lo Two = One -- 0 mod 2
  type Hi Two = One -- 1 mod 2

instance Split (Succ n) where
  type Lo (Succ n) = Lo (n)  
  type Hi (Succ n) = Succ (Hi n)

Two est défini comme Succ One, et les synonymes de type simple sont développés à des fins d'égalité syntaxique, ils sont donc égaux sur les côtés gauches ;mais les membres de droite ne le sont pas, d’où l’erreur.

Vous avez peut-être remarqué que j'ai supprimé le contexte de classe du code ci-dessus.Le problème le plus profond, et peut-être la raison pour laquelle vous ne vous attendiez pas à ce que le conflit ci-dessus se produise, est que les instances en double sont doublons contradictoires.Les contextes de classe sont, comme toujours, ignorés à des fins de sélection d'instances, et si ma mémoire est bonne, cela est double pour les familles de types associées, qui sont en grande partie une commodité syntaxique pour les familles de types non associées et peuvent ne pas être contraintes par la classe comme vous le feriez. attendre.

Maintenant, clairement, ces deux cas devrait être distincts, et vous aimeriez choisir entre eux en fonction du résultat de l'utilisation Compare, donc ce résultat doit être un paramètre de la classe de type, pas simplement une contrainte.Vous mélangez également ici des familles de types avec des dépendances fonctionnelles, ce qui est inutilement gênant.Ainsi, en commençant par le haut, nous conserverons les types de base :

-- type-level naturals
data One
data Succ n 
type Two = Succ One

-- type-level ordering
data LT
data EQ
data GT

Réecrit le Compare fonctionner comme une famille de types :

type family Compare n m :: *
type instance Compare One One = EQ
type instance Compare (Succ n) One = GT
type instance Compare One (Succ n) = LT
type instance Compare (Succ n) (Succ m) = Compare n m

Maintenant, pour gérer le conditionnel, nous aurons besoin d’une sorte de famille de types « contrôle de flux ».Je vais définir ici quelque chose d'un peu plus général pour l'édification et l'inspiration ;spécialiser selon les goûts.

Nous allons lui donner un prédicat, une entrée et deux branches parmi lesquelles choisir :

type family Check pred a yes no :: * 

Nous aurons besoin d'un prédicat pour tester Comparele résultat :

data CompareAs a
type instance (CompareAs LT) LT yes no = yes 
type instance (CompareAs EQ) LT yes no = no
type instance (CompareAs GT) LT yes no = no
type instance (CompareAs LT) EQ yes no = no 
type instance (CompareAs EQ) EQ yes no = yes
type instance (CompareAs GT) EQ yes no = no
type instance (CompareAs LT) GT yes no = no
type instance (CompareAs EQ) GT yes no = no
type instance (CompareAs GT) GT yes no = yes

C'est un ensemble de définitions terriblement fastidieux, certes, et le pronostic est assez sombre pour comparer des ensembles plus larges de valeurs de type.Des approches plus extensibles existent (une balise pseudo-genre et une bijection avec les naturels étant une solution évidente et efficace) mais cela dépasse un peu la portée de cette réponse.Je veux dire, nous faisons juste du calcul au niveau du type ici, n'allons pas ridicule Ou n'importe quoi.

Plus simple dans ce cas serait simplement de définir une fonction d’analyse de cas sur les résultats de comparaison :

type family CaseCompare cmp lt eq gt :: *
type instance CaseCompare LT lt eq gt = lt
type instance CaseCompare EQ lt eq gt = eq
type instance CaseCompare GT lt eq gt = gt

J'utiliserai cette dernière pour l'instant, mais si vous souhaitez des conditions plus complexes ailleurs, une approche générique commence à avoir plus de sens.

De toute façon.Nous pouvons diviser le...euh, Split classer en familles de types non associées :

data Oops

type family Lo n :: *
type instance Lo Two = One
type instance Lo (Succ (Succ n)) 
    = CaseCompare (Compare (Lo (Succ n)) (Hi (Succ n)))
                  Oops -- yay, type level inexhaustive patterns
                  (Succ n)
                  (Lo (Succ n))

type family Hi n :: *
type instance Hi Two = One
type instance Hi (Succ (Succ n)) 
    = CaseCompare (Compare (Lo (Succ n)) (Hi (Succ n)))
                  Oops -- yay, type level inexhaustive patterns
                  One
                  (Succ (Hi (Succ n)))

Le point le plus significatif ici est l’utilisation (apparemment redondante) de (Succ (Succ n))--la raison en est que deux Succ les constructeurs sont nécessaires pour distinguer l'argument de Two, évitant ainsi les erreurs de conflit que vous avez vues.

Notez que j'ai tout déplacé ici pour taper des familles pour plus de simplicité, car tout est entièrement au niveau du type.Si vous souhaitez également gérer les valeurs différemment en fonction des calculs ci-dessus, y compris indirectement, via le Mod type : vous devrez peut-être rajouter les définitions de classe appropriées, car celles-ci sont nécessaires pour choisir les termes en fonction du type, plutôt que de simplement choisir les types en fonction des types.