Отключить принуждение типа Haskell

Question

У меня есть пример на основе hyperloglog. Я пытаюсь параметризовать мой Container с размером и использовать reflection, чтобы использовать этот параметр в функциях на контейнерах.

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 

Мой хромой Monoid экземпляр определяет mempty на основе овеществленной параметры, и делать некоторые «типобезопасные» mappend. Он отлично работает, когда я пытаюсь суммировать контейнеры разного размера, с ошибкой типа.

Однако он по-прежнему может быть обманут с coerce, и я ищу способ блокировать его во время компиляции:

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]} 

Добавление типа роли не помогает

type role Container nominal 

Answer 1

этот вопрос заключается в том, что newtype s являются коэрцибелами к их представлению до тех пор, пока конструктор находится в сфере действия - действительно, это большая часть мотивации для Coercible. А ограничения Coercible похожи на любые ограничения типа класса, и их автоматически ищут и объединяют для вас, тем более. Таким образом, coerce c3 находит, что у вас есть

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

для всех p и p' и счастливо строить композитное принуждение для вас через

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

Если вы не экспортировать Container конструктора - как вы, вероятно, хочу все равно! - то это уже не известно, что newtype равно его представления (вы потеряете первые два экземпляра выше), и вы получите нужную ошибку в других модулях:

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 

Однако, вы всегда будете иметь возможность разбейте свои инварианты в модуле, где вы определяете newtype (через coerce или иначе).

---

В качестве примечания, вы, вероятно, не хотите использовать аксессор запись стиле здесь и экспортировать его; который позволяет пользователям использовать синтаксис обновления записи, чтобы изменить код из-под вас, поэтому

c3 :: Container 3 
c3 = mempty 

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

действителен. Вместо этого сделайте runContainer отдельно стоящей функцией.

---

Мы можем убедиться, что мы получаем состав двух newtype -представлением ограничений, глядя на Ядра (через -ddump-simpl): внутри модуля, который определяет Container (который я также называется Container), выход (если мы удалим список экспорта)

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) 

это немного трудно читать, но главное, чтобы увидеть это Container.NTCo:Container[0]: NTCo является newtype принуждения между newtypeContainer p и этим тип представления.Sym вращает это, и ; составляет два ограничения.

Вызовите окончательное ограничение γₓ; то весь типирование вывод является

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 
γₓ = γ₃ ; γ₄′ 

---

Вот исходные файлы, которые я использовал:

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