9
Tôi có thể thề rằng tôi đã xem một bài viết về điều này gần đây, nhưng tôi không thể tìm thấy nó.Haskell/GHC: Cách viết các biến vị ngữ trên các loại naturals loại
Tôi đang cố gắng để tạo ra một loại để làm mã hóa nhị phân của những con số mod n, nhưng làm như vậy, tôi cần phải có khả năng viết các vị từ trên Naturals mức loại:
{-# 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
My hiện tại triển khai thực hiện trích xuất một loạt lỗi trình biên dịch:
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
Điều này khiến tôi nghĩ rằng tôi sẽ viết sai vị ngữ của tôi nếu chúng cho rằng chúng xung đột.
Tôi làm cách nào để làm đúng?
Bằng "naturals", ý bạn là "số tự nhiên"? – Charles
Loại gia đình và các trường hợp trùng lặp không hoạt động cùng nhau ngay bây giờ. Xem qua tại http://hackage.haskell.org/trac/ghc/ticket/4259 –