Jak wdrożyć liczb binarnych w Haskell

Question

Widziałem następujące konstruktora danych dla cyframi kościelnych

data Nat = Zero | Succ Nat deriving Show 

Ale to numery unarne. W jaki sposób zaimplementujemy konstruktor danych dla liczb binarnych w Haskell?

Próbowałem to:

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

Po tym możemy uzyskać, dziesiętny 5 zakodowany jako BinC [One,Zero,One]

Ale myślę, że jestem brakuje czegoś tutaj. Moje rozwiązanie wydaje się nie tak sprytne jak rozwiązanie Kościoła. Nic dziwnego, nie jestem Kościołem. Trochę myślenia, stwierdziłem, że moje rozwiązanie zależy od listy, podczas gdy Nat nie zależy od takiej zewnętrznej struktury, takiej jak lista.

Czy możemy napisać rozwiązanie podobne do używanego przez Kościół przy użyciu konstruktora typu Succ również dla liczb binarnych? Jeśli tak, w jaki sposób? Próbowałem dużo, ale wydaje się, że mój mózg nie może pozbyć się potrzeby listy lub jakiejś innej takiej struktury.

Answer 1

Najbliżej mogę myśleć byłoby coś

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

To sprawia, że ​​możliwe jest skonstruowanie liczb binarnych robi tylko

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

Można by również wyobrazić funkcją dekodowania pracy na zasada (znacznie lepsza wersja sugerowana przez Ingo w komentarzach)

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

Który może być następnie użyty do dekodowania liczby binarnej na liczbę całkowitą.

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

---

Trudność z tym, co chcesz osiągnąć to, że trzeba czytać liczby binarne „inside out” lub tak powiem. Aby poznać wartość najbardziej znaczącej cyfry, musisz wiedzieć, ile cyfr masz w numerze. Gdybyś zapisywał swoje liczby binarne w "odwrocie" - tj. Najbardziej zewnętrzna cyfra jest najmniej znaczącą cyfrą, wtedy rzeczy byłyby dużo łatwiejsze w obsłudze, ale liczby wyglądałyby wstecz po ich utworzeniu i wydrukowaniu za pomocą domyślnej instancji z Show.

Przyczyną tego nie jest problem z liczbami jednoznacznymi, ponieważ nie ma "najmniej znaczącej cyfry", ponieważ wszystkie cyfry mają tę samą wartość, więc można przeanalizować liczbę z obu kierunków, a otrzymasz taki sam wynik.

---

Dla kompletności, tutaj jest to samo, ale z cyfrą najbardziej zewnętrzna jest najmniej znacząca cyfra:

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

To wygląda prawie jak poprzednio, ale można zauważyć, że gdy funkcja dekodowania jest zaimplementowane,

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

Liczby są zapisane wstecz!

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

Jest to jednak o wiele łatwiejsze w obsłudze. Możemy na przykład dodać dwie liczby binarne osobno dla każdego przypadku. (Uwaga: wiele przypadków)

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

W tym momencie dodawania dwóch liczb binarnych jest bardzo proste:

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

I rzeczywiście!

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

tylko dodatkiem do innych odpowiedzi już otrzymali:

Wartości danych, które są rzeczywiście cyfry tworzące Peano, nie liczebników Kościoła. Są blisko spokrewnione, ale w rzeczywistości są dual/odwrotne względem siebie. Liczby Peano opierają się na pojęciu konstruowania liczb poza pojęciem zbioru, który w Haskell używamy ściśle powiązanej koncepcji typu danych do przedstawienia.

{-# LANGUAGE RankNTypes #-} 

import Prelude hiding (succ) 

data Peano = Zero 
      | Succ Peano 
    deriving (Show) 

cyfry Church, z drugiej strony, kodowanie cyfr jako funkcji:

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

zero :: Church 
zero = \p -> id 

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

Teraz można umieścić je razem:

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 

Więc Kościół cyfry są w istocie, krotnie nad cyframi Peano! I (peano . church) jest identyfikatorem dla liczb Peano, chociaż z typami podanymi powyżej Haskell nie pozwoli ci bezpośrednio je skomponować w ten sposób. Jeśli pominiesz deklaracje typu, Haskell zasugeruje wystarczająco ogólne typy, że będziesz w stanie je skomponować.

Istnieje ładny przegląd różnicy i ich wzajemnego związku w kontekście programowania funkcjonalnego w Perła teoretyczna Ralfa Hinze'a Church numerals, twice!.

Możesz jeszcze bardziej uogólnić tę dwoistość; Liczby Peano są w zasadzie początkową F-Algebrą dla liczb naturalnych, a cyfry Kościoła są zasadniczo końcową/końcową F-węglem dla liczb naturalnych. Dobrym wstępem do tego jest Bart Jacobs i Jan Rutten A Tutorial on (Co)Algebras and (Co)Induction.