Vô hiệu hóa cưỡng ép kiểu Haskell

Question

Tôi có ví dụ dựa trên hyperloglog. Tôi đang cố gắng để parametrize của tôi Container với kích thước, và sử dụng reflection để sử dụng tham số này trong các chức năng trên container.

import   Data.Proxy 
import   Data.Reflection 

newtype Container p = Container { runContainer :: [Int] } 
    deriving (Eq, Show) 

instance Reifies p Integer => Monoid (Container p) where 
    mempty = Container $ replicate (fromIntegral (reflect (Proxy :: Proxy p))) 0 
    mappend (Container l) (Container r) = undefined 

dụ monoid què của tôi định nghĩa mempty dựa trên tham số reified, và làm một số "kiểu an" mappend. Nó hoạt động hoàn hảo khi tôi đang cố gắng để tổng hợp các container có kích thước khác nhau, không có lỗi kiểu.

Tuy nhiên nó vẫn có thể bị lừa với coerce, và tôi đang tìm cách để ngăn chặn nó ở thời gian biên dịch:

ghci> :set -XDataKinds 
ghci> :m +Data.Coerce 
ghci> let c3 = mempty :: Container 3 
ghci> c3 
ghci> Container {runContaner: [0,0,0]} 
ghci> let c4 = coerce c3 :: Container 4 
ghci> :t c4 
ghci> c4 :: Container 4 
ghci> c4 
ghci> Container {runContainer: [0,0,0]} 

Thêm loại vai trò không giúp

type role Container nominal 

Answer 1

Vấn đề này là newtype s có thể cưỡng chế được với biểu diễn của chúng miễn là hàm tạo nằm trong phạm vi - thực sự, đây là một phần quan trọng trong động lực cho Coercible. Và ràng buộc Coercible giống như bất kỳ ràng buộc loại lớp nào khác và được tự động tìm kiếm và đặt cùng nhau cho bạn, thậm chí còn nhiều hơn thế nữa. Như vậy, coerce c3 được thấy rằng bạn có

instance Coercible (Container p) [Int] 
instance Coercible [Int] (Container p') 

cho tất cả p và p', và hạnh phúc xây dựng cưỡng chế composite cho bạn qua

instance (Coercible a b, Coercible b c) => Coercible a c 

Nếu bạn không xuất constructor Container - như bạn có thể muốn làm gì! - sau đó nó không còn biết rằng newtype bằng đại diện của mình (bạn bị mất hai trường hợp đầu tiên ở trên), và bạn nhận được lỗi mong muốn trong các module khác:

ContainerClient.hs:13:6: 
    Couldn't match type ‘4’ with ‘3’ 
    arising from trying to show that the representations of 
     ‘Container 3’ and 
     ‘Container 4’ are the same 
    Relevant role signatures: type role Container nominal nominal 
    In the expression: coerce c3 
    In an equation for ‘c4’: c4 = coerce c3 

Tuy nhiên, bạn sẽ luôn luôn có thể phá vỡ bất biến của bạn trong mô-đun nơi bạn xác định newtype (qua coerce hoặc cách khác).

---

Như một mặt lưu ý, bạn có thể không muốn sử dụng một accessor kỷ phong cách ở đây và xuất khẩu nó; cho phép người dùng sử dụng cú pháp cập nhật bản ghi để thay đổi mã từ bên dưới bạn, do đó,

c3 :: Container 3 
c3 = mempty 

c3' :: Container 3 
c3' = c3{runContainer = []} 

trở nên hợp lệ. Thay vào đó, hãy tạo runContainer chức năng tự do.

---

Chúng ta có thể xác minh rằng chúng tôi đang nhận được các thành phần của hai newtype -representation hạn chế bằng cách nhìn vào Core (qua -ddump-simpl): trong module định nghĩa Container (mà tôi cũng đã gọi Container), đầu ra là (nếu chúng ta loại bỏ các danh sách xuất khẩu)

c4 :: Container 4 
[GblId, Str=DmdType] 
c4 = 
    c3 
    `cast` (Container.NTCo:Container[0] <GHC.TypeLits.Nat>_N <3>_N 
      ; Sym (Container.NTCo:Container[0] <GHC.TypeLits.Nat>_N <4>_N) 
      :: Container 3 ~R# Container 4) 

đó là một chút khó khăn để đọc, nhưng điều quan trọng để xem là Container.NTCo:Container[0]: các NTCo là một sự ép buộc newtype giữa newtypeContainer p và nó s đại diện loại.Sym xoay vòng này và ; soạn hai ràng buộc.

Gọi ràng buộc cuối cùng γₓ; sau đó toàn bộ nguồn gốc gõ là

Sym :: (a ~ b) -> (b ~ a) 
-- Sym is built-in 

(;) :: (a ~ b) -> (b ~ c) -> (a ~ c) 
-- (;) is built-in 

γₙ :: k -> (p :: k) -> Container p ~ [Int] 
γₙ k p = Container.NTCo:Container[0] <k>_N <p>_N 

γ₃ :: Container 3 ~ [Int] 
γ₃ = γₙ GHC.TypeLits.Nat 3 

γ₄ :: Container 4 ~ [Int] 
γ₄ = γₙ GHC.TypeLits.Nat 4 

γ₄′ :: [Int] ~ Container 4 
γ₄′ = Sym γ₄ 

γₓ :: Container 3 ~ Container 4 
γₓ = γ₃ ; γ₄′ 

---

Dưới đây là các tập tin nguồn tôi đã sử dụng:

Container.hs:

{-# LANGUAGE FlexibleContexts, UndecidableInstances, ScopedTypeVariables, 
      RoleAnnotations, PolyKinds, DataKinds #-} 

module Container (Container(), runContainer) where 

import Data.Proxy 
import Data.Reflection 
import Data.Coerce 

newtype Container p = Container { runContainer :: [Int] } 
    deriving (Eq, Show) 
type role Container nominal 

instance Reifies p Integer => Monoid (Container p) where 
    mempty = Container $ replicate (fromIntegral (reflect (Proxy :: Proxy p))) 0 
    mappend (Container l) (Container r) = Container $ l ++ r 

c3 :: Container 3 
c3 = mempty 

-- Works 
c4 :: Container 4 
c4 = coerce c3 

ContainerClient.hs:

{-# LANGUAGE DataKinds #-} 

module ContainerClient where 

import Container 
import Data.Coerce 

c3 :: Container 3 
c3 = mempty 

-- Doesn't work :-) 
c4 :: Container 4 
c4 = coerce c3