Haskell/GHC: come scrivere predicati su naturali a livello di tipo

Question

Avrei potuto giurare di aver visto un articolo su questo di recente, ma non riesco a trovarlo.

Sto cercando di creare un tipo per fare la codifica binaria dei numeri mod n, ma per farlo, devo essere in grado di scrivere predicati a livello di tipo naturale:

{-# 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

La mia attuale implementazione sputa un sacco di errori del compilatore:

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

Il che mi fa pensare che sto scrivendo i miei predicati sbagliati, se pensa che siano in conflitto.

Come posso farlo bene?

Answer 1

Il problema del conflitto è abbastanza semplice. Il Regole per famiglie di tipo sovrapposto sono abbastanza semplici:

Le dichiarazioni di istanza di una famiglia di tipo utilizzata in un singolo programma possono sovrapporsi solo se i lati di destra delle istanze sovrapposte coincidono per i tipi sovrapposti. Più formalmente, due dichiarazioni di istanza si sovrappongono se esiste una sostituzione che rende sintatticamente uguali i lati a sinistra delle istanze. Ogni volta che è così, i lati di destra delle istanze devono anche essere sintatticamente uguali sotto la stessa sostituzione.

Si noti che specifica sintatticamente pari. Considera queste due istanze:

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 è definito come Succ One, e i sinonimi di tipo semplice sono ampliati ai fini dell'uguaglianza sintattica, quindi questi sono uguali sui lati a sinistra; Ma i lati a destra non lo sono, quindi l'errore.

Potresti aver notato che ho rimosso il contesto della classe dal codice sopra. Il problema più profondo, e forse perché non ti aspettavi che si verifichi il conflitto di cui sopra, è che le istanze duplicate sono Duplicati contrastanti. I contesti di classe sono, come sempre, ignorati ai fini della selezione delle istanze, e se la memoria mi serve questo è il doppio per le famiglie di tipo associato, che sono in gran parte una comodità sintattica per le famiglie di tipo non associato e potrebbero non essere vincolati dalla classe in modi che faresti aspettare.

Ora, chiaramente quei due casi dovrebbe Sii distinto e vorresti scegliere tra loro in base al risultato dell'uso Compare, quindi quel risultato deve essere un parametro della classe di tipo, non solo un vincolo. Stai anche mescolando famiglie di tipo con dipendenze funzionali qui, che è inutilmente imbarazzante. Quindi, a partire dall'alto, manterremo i tipi di base:

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

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

Riscrivi il Compare Funzionare come una famiglia di tipi:

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

Ora, per gestire il condizionale avremo bisogno di una sorta di famiglia di tipo "Controllo a flusso". Definerò qualcosa di un po 'più generale qui per l'edificazione e l'ispirazione; specializzato in base al gusto.

Gli daremo un predicato, un input e due rami da scegliere da:

type family Check pred a yes no :: * 

Avremo bisogno di un predicato per il test CompareRisultato:

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

È una serie di definizioni spaventosamente noiose, concessa, e la prognosi è piuttosto cupa per confrontare set più grandi di valori di tipo. Esistono approcci più estensibili (un tag pseudo-gentile e una biiezione con i naturali che sono una soluzione ovvia ed efficace) ma è un po 'oltre lo scopo di questa risposta. Voglio dire, stiamo solo facendo il calcolo a livello di tipo qui, non otteniamo ridicolo o altro.

Più semplice in questo caso sarebbe semplicemente definire una funzione di analisi del caso sui risultati del confronto:

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

Per ora userò quest'ultimo, ma se vuoi condizionamenti più complessi altrove un approccio generico inizia a avere più senso.

Comunque. Possiamo dividere il ... ehm, Split Classe in famiglie di tipo non associata:

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)))

Il punto più significativo qui è l'uso (apparentemente ridondante) (Succ (Succ n))-Il motivo di ciò è che due Succ I costruttori sono necessari per distinguere l'argomento Two, evitando così gli errori di conflitto che hai visto.

Nota che ho spostato tutto per digitare le famiglie qui per semplicità, poiché è tutto interamente a livello di tipo. Se si desidera anche gestire i valori in modo diverso a seconda dei calcoli di cui sopra, incluso indirettamente, tramite il Mod Tipo: potrebbe essere necessario aggiungere le definizioni di classe appropriate, poiché sono necessarie per la scelta dei termini in base al tipo, piuttosto che semplicemente scegliere i tipi in base a tipi.