Come implementare i numeri binari in Haskell

Question

Ho visto il seguente costruttore di dati per numeri Chiesa

data Nat = Zero | Succ Nat deriving Show 

Ma questo è numeri unari. Come implementiamo un costruttore di dati per i numeri binari in Haskell in questo modo?

Ho provato questo:

data Bin = Zero | One | BinC [Bin] deriving Show 

Dopo questo siamo in grado di ottenere, decimale 5 codificato come BinC [One,Zero,One]

Ma penso che mi manca qualcosa qui. La mia soluzione non sembra intelligente come la soluzione della Chiesa. Nessuna sorpresa, non sono Chiesa. Un po 'di pensiero, ho trovato che la mia soluzione dipende dalla lista, mentre il Nat non dipende da nessuna di queste strutture esterne come la lista.

Possiamo scrivere una soluzione simile a quella di Church che utilizza un costruttore di tipo Succ anche per i numeri binari? Se sì, come? Ho provato molto, ma sembra che il mio cervello non possa eliminare il bisogno di elencare o qualche altra struttura del genere.

Answer 1

Il più vicino mi viene in mente sarebbe qualcosa di simile

λ> data Bin = LSB | Zero Bin | One Bin 
λ| -- deriving Show 

In questo modo è possibile costruire i numeri binari facendo proprio

λ> One . One . Zero . Zero . One . One $ LSB 
One (One (Zero (Zero (One (One LSB))))) 

si potrebbe anche immaginare una funzione di decodifica lavorare su il principio di (versione molto migliore suggerita da Ingo nei commenti)

λ> let toInt :: (Integral a) => Bin -> a 
λ|  toInt = flip decode 0 
λ|  where decode :: (Integral a) => Bin -> a -> a 
λ|    decode LSB value = value 
λ|    decode (Zero rest) value = decode rest (2*value) 
λ|    decode (One rest) value = decode rest (2*value + 1) 

Quale può quindi essere utilizzato per decodificare un numero binario in un numero intero.

λ> toInt (Zero . One . One . One . Zero . Zero . One $ LSB) 
57 

---

La difficoltà con quello che si vuole realizzare è che avete bisogno di leggere i numeri binari "dentro e fuori", o per così dire. Per conoscere il valore della cifra più significativa, devi sapere quante cifre hai nel numero. Se dovessi scrivere i tuoi numeri binari in "reverse" - cioè la cifra più esterna è la cifra meno significativa, allora le cose sarebbero molto più facili da gestire ma i numeri guarderebbero all'indietro quando li crei e li stampi usando l'istanza predefinita di Show.

Il motivo per cui questo non è un problema con i numeri unari è perché non esiste una "cifra meno significativa" poiché tutte le cifre hanno lo stesso valore, quindi è possibile analizzare il numero da entrambe le direzioni e si otterrà lo stesso risultato.

---

Per completezza, qui è la stessa cosa, ma con la cifra più esterno essendo la cifra meno significativa:

λ> data Bin = MSB | Zero Bin | One Bin 
λ| -- deriving Show 

che sembra più o meno come prima, ma si noterà che quando la funzione di decodifica è implementato,

λ> let toInt = flip decode (1,0) 
λ|  where 
λ|   decode (One rest) (pos, val) = decode rest (pos*2, val+pos) 
λ|   decode (Zero rest) (pos, val) = decode rest (pos*2, val) 
λ|   decode MSB (_, val) = val 

I numeri sono scritti all'indietro!

λ> toInt (Zero . Zero . Zero . One . Zero . One $ MSB) 
40 

Tuttavia, questo è molto più facile da gestire. Ad esempio, possiamo aggiungere due numeri binari caso per caso. (Attenzione: un sacco di casi)

λ> let add a b = addWithCarry a b False 
λ|  where 
λ|  addWithCarry :: Bin -> Bin -> Bool -> Bin 
λ|  addWithCarry MSB MSB True = One MSB 
λ|  addWithCarry MSB MSB False = MSB 
λ|  addWithCarry MSB b c = addWithCarry (Zero MSB) b c 
λ|  addWithCarry a MSB c = addWithCarry a (Zero MSB) c 
λ|  addWithCarry (Zero restA) (Zero restB) False = Zero (addWithCarry restA restB False) 
λ|  addWithCarry (One restA) (Zero restB) False = One (addWithCarry restA restB False) 
λ|  addWithCarry (Zero restA) (One restB) False = One (addWithCarry restA restB False) 
λ|  addWithCarry (One restA) (One restB) False = Zero (addWithCarry restA restB True) 
λ|  addWithCarry (Zero restA) (Zero restB) True = One (addWithCarry restA restB False) 
λ|  addWithCarry (One restA) (Zero restB) True = Zero (addWithCarry restA restB True) 
λ|  addWithCarry (Zero restA) (One restB) True = Zero (addWithCarry restA restB True) 
λ|  addWithCarry (One restA) (One restB) True = One (addWithCarry restA restB True) 

A quel punto l'aggiunta di due numeri binari è un gioco da ragazzi:

λ> let forty = Zero . Zero . Zero . One . Zero . One $ MSB 
λ|  eight = Zero . Zero . Zero . One $ MSB 
λ| 
λ> add forty eight 
Zero (Zero (Zero (Zero (One (One MSB))))) 

E in effetti!

λ> toInt $ Zero (Zero (Zero (Zero (One (One MSB))))) 
48 

Answer 2

data Bit = Zero | One 
data Bin = E Bit | S Bit Bin 

five = S One (S Zero (E One)) 

Answer 3

Basta un addendum alle altre risposte che hai ricevuto:

I valori dei dati che si sta creando sono in realtà numeri Peano, non numeri Chiesa. Sono strettamente correlati, ma in realtà sono duali/inversi l'uno rispetto all'altro. I numeri di Peano sono costruiti sulla nozione di costruire numeri fuori dal concetto di un Set, che in Haskell usiamo il concetto strettamente correlato di un tipo di dati da rappresentare.

{-# LANGUAGE RankNTypes #-} 

import Prelude hiding (succ) 

data Peano = Zero 
      | Succ Peano 
    deriving (Show) 

numeri della Chiesa, d'altra parte, codificano numeri come funzioni:

type Church = forall n. (n -> n) -> n -> n 

zero :: Church 
zero = \p -> id 

succ :: Church -> Church 
succ = \n p -> p . n p 

Ora, è possibile metterli insieme:

peano :: Church -> Peano 
peano c = c Succ Zero 

fold :: forall n. (n -> n) -> n -> Peano -> n 
fold s z Zero  = z 
fold s z (Succ p) = s (fold s z p) 

church :: Peano -> Church 
church p = \s z -> fold s z p 

Così la Chiesa numeri sono, in sostanza, una piega sui numeri di Peano! E (peano . church) è l'identità per i numeri di Peano, sebbene con i tipi dati come sopra Haskell non ti consente di comporli direttamente in questo modo. Se si omettono le dichiarazioni di tipo, Haskell dedurrà tipi abbastanza generali che sarete in grado di comporli.

C'è una bella panoramica della differenza e del loro rapporto reciproco nel contesto della programmazione funzionale qui in Theoretical Pearl di Ralf Hinze Church numerals, twice!.

È possibile generalizzare ulteriormente questa dualità; i numeri di Peano sono essenzialmente l'algebra F iniziale per i numeri naturali e i numeri di Chiesa sono essenzialmente la F-coalgebra finale/terminale per i numeri naturali. Una buona introduzione a questo è di Bart Jacobs e Jan Rutten A Tutorial on (Co)Algebras and (Co)Induction.