Làm thế nào để thực hiện số nhị phân trong Haskell

Question

Tôi đã thấy các nhà xây dựng dữ liệu sau cho chữ số Giáo Hội

data Nat = Zero | Succ Nat deriving Show 

Nhưng đây là số unary. Làm cách nào để chúng tôi triển khai một hàm tạo dữ liệu cho các số nhị phân trong Haskell theo cách này?

Tôi đã thử này:

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

Sau này chúng ta có thể nhận được, số thập phân 5 mã hóa như BinC [One,Zero,One]

Nhưng tôi nghĩ rằng tôi đang thiếu một cái gì đó ở đây. Giải pháp của tôi dường như không thông minh như giải pháp của Giáo Hội. Không ngạc nhiên, tôi không phải là Giáo Hội. Một chút suy nghĩ, tôi thấy rằng giải pháp của tôi phụ thuộc vào danh sách, trong khi Nat không phụ thuộc vào bất kỳ cấu trúc bên ngoài như danh sách.

Chúng ta có thể viết một giải pháp tương tự như của Giáo Hội bằng cách sử dụng hàm tạo kiểu Succ cho số nhị phân không? Nếu có, làm thế nào? Tôi đã thử rất nhiều, nhưng có vẻ như bộ não của tôi không thể thoát khỏi sự cần thiết của danh sách hoặc một số cấu trúc như vậy.

Answer 1

Gần nhất tôi có thể nghĩ đến sẽ là một cái gì đó giống như

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

Điều này làm cho nó có thể để xây dựng số nhị phân làm chỉ

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

Người ta cũng có thể tưởng tượng một chức năng giải mã làm việc trên nguyên tắc của (phiên bản tốt hơn được đề xuất bởi Ingo trong các ý kiến)

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

Mà sau đó có thể được sử dụng để giải mã một số nhị phân thành một số nguyên.

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

---

Khó khăn với những gì bạn muốn đạt được là bạn cần phải đọc số nhị phân "từ trong ra ngoài", hay như vậy để nói chuyện. Để biết giá trị của chữ số quan trọng nhất, bạn cần phải biết số lượng chữ số bạn có trong số đó. Nếu bạn viết các số nhị phân của mình bằng "ngược" - tức là chữ số ngoài cùng là chữ số ít quan trọng nhất, thì mọi thứ sẽ dễ xử lý hơn nhưng các con số sẽ nhìn ngược lại khi bạn tạo chúng và in chúng ra bằng cách sử dụng thể hiện mặc định của Show.

Lý do đây không phải là vấn đề với số đơn là vì không có "chữ số có nghĩa nhỏ nhất" vì tất cả các chữ số có cùng giá trị, vì vậy bạn có thể phân tích số từ hai hướng và bạn sẽ nhận được kết quả tương tự.

---

Để hoàn chỉnh, đây là điều tương tự nhưng với chữ số ngoài cùng là chữ số có ý nghĩa nhất:

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

Điều đó có vẻ khá nhiều như trước đây, nhưng bạn sẽ nhận thấy rằng khi các chức năng giải mã được triển khai,

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

Số được viết ngược!

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

Tuy nhiên, điều này dễ xử lý hơn nhiều. Ví dụ, chúng ta có thể thêm hai số nhị phân trên cơ sở từng trường hợp. (Cảnh báo: rất nhiều trường hợp)

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

Tại thời điểm đó thêm hai số nhị phân là một làn gió:

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

Và quả thật vậy!

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

Chỉ cần một phụ lục cho câu trả lời khác mà bạn đã nhận:

Các giá trị dữ liệu bạn đang tạo thực sự Peano chữ số, không phải chữ số Giáo Hội. Chúng có liên quan chặt chẽ, nhưng chúng thực sự là nhị phân/nghịch đảo với nhau. Các số Peano được xây dựng dựa trên khái niệm xây dựng các con số trong khái niệm của một Set, mà trong Haskell chúng ta sử dụng khái niệm liên quan chặt chẽ của một kiểu dữ liệu để biểu diễn.

{-# LANGUAGE RankNTypes #-} 

import Prelude hiding (succ) 

data Peano = Zero 
      | Succ Peano 
    deriving (Show) 

chữ số Giáo Hội, mặt khác, mã hóa chữ số như chức năng:

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

zero :: Church 
zero = \p -> id 

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

Bây giờ, bạn có thể đặt chúng lại với nhau:

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 

Vì vậy, Giáo Hội chữ số là, về bản chất, một số gấp qua số Peano! Và (peano . church) là danh tính cho số Peano, mặc dù với các loại được đưa ra như trên Haskell sẽ không cho phép bạn trực tiếp soạn chúng như thế. Nếu bạn loại bỏ các khai báo kiểu, Haskell sẽ phỏng đoán các kiểu chung đủ để bạn có thể soạn chúng.

Có tổng quan tốt đẹp về sự khác biệt và mối quan hệ của chúng với nhau trong ngữ cảnh lập trình chức năng ở đây trong Pearl lý thuyết Ralf Hinze Church numerals, twice!.

Bạn có thể khái quát hóa tính hai mặt này hơn nữa; các số Peano về cơ bản là đại số F ban đầu cho các số tự nhiên và các chữ số của Giáo hội về bản chất là F-coalgebra cuối cùng/đầu cuối cho các số tự nhiên. Một giới thiệu tốt về điều này là của Bart Jacobs 'và Jan Rutten's A Tutorial on (Co)Algebras and (Co)Induction.