Có thể thực hiện thủ thuật của Data.Reflection bằng cách sử dụng các loại gia đình thay vì fundeps không?

Question

Việc triển khai GHC của Data.Reflection từ gói sử dụng một mẹo liên quan đến unsafeCoerce tận dụng lợi thế của cách GHC biên soạn typeclasses bằng cách sử dụng từ điển đi qua. Việc thực hiện ngắn, vì vậy tôi có thể tái tạo nó một cách trọn vẹn ở đây:

class Reifies s a | s -> a where 
    reflect :: proxy s -> a 

newtype Magic a r = Magic (forall (s :: *). Reifies s a => Proxy s -> r) 

reify :: forall a r. a -> (forall (s :: *). Reifies s a => Proxy s -> r) -> r 
reify a k = unsafeCoerce (Magic k :: Magic a r) (const a) Proxy 

Điều này làm cho nó có thể cụ thể hóa một giá trị ở cấp loại, sau đó phản ánh nó trở lại:

ghci> reify (42 :: Integer) (\p -> reflect p) :: Integer 
42 

Tôi đã quan tâm khi sử dụng kỹ thuật này, nhưng tôi nghĩ sẽ thuận tiện cho mục đích sử dụng gia đình kiểu của mình với số Reifies thay vì phụ thuộc chức năng, vì vậy tôi đã cố gắng viết lại quá trình triển khai bằng cách sử dụng phép biến đổi thông thường:

class Reifies s where 
    type Reflects s 
    reflect :: Proxy s -> Reflects s 

newtype Magic a r = Magic (forall (s :: *). (Reifies s, Reflects s ~ a) => Proxy s -> r) 

reify :: forall a r. a -> (forall (s :: *). (Reifies s, Reflects s ~ a) => Proxy s -> r) -> r 
reify a k = unsafeCoerce (Magic k :: Magic a r) (const a) Proxy 

Đáng buồn thay, tuy nhiên, điều này không còn hoạt động! Điều này thay đổi quá trình biên soạn đủ để phá vỡ thủ thuật unsafeCoerce:

ghci> reify (42 :: Integer) (\p -> reflect p) :: Integer 
2199023255808 

Tuy nhiên, tôi không quen với cách GHC hoạt động để hiểu tại sao. Có thể triển khai Data.Reflection bằng cách sử dụng loại được liên kết thay vì phụ thuộc chức năng không? Nếu có, cần thay đổi điều gì? Nếu không, tai sao không?

Answer 1

Bí quyết unsafeCoerce lợi dụng thực tế là

Reifies s a => Proxy s -> r 

có chính xác các đại diện tương tự, tại thời gian chạy, như

a -> Proxy s -> r 

Bằng cách mở rộng các hạn chế để (Reifies s a, a ~ Reflects s), bạn vi phạm quan trọng này giả định. Có một số cách để khắc phục điều này. Dưới đây là một:

{-# language MultiParamTypeClasses, TypeFamilies, PolyKinds, KindSignatures, 
     RankNTypes, ScopedTypeVariables, TypeOperators #-} 
module TFReifies where 
import Data.Proxy 
import Unsafe.Coerce 
import Data.Type.Equality 

class Reifies s a where 
    type Reflects s :: * 
    reflect' :: proxy s -> a 

reflect :: (Reifies s a, a ~ Reflects s) => proxy s -> a 
reflect = reflect' 


newtype Magic a r = Magic (forall (s :: *). (Reifies s a) => Proxy s -> r) 

reify' :: forall a r. a -> (forall (s :: *). (Reifies s a) => Proxy s -> r) -> r 
reify' a k = unsafeCoerce (Magic k :: Magic a r) (const a) Proxy 

reify :: forall a r. a -> (forall (s :: *). (Reifies s a, a ~ Reflects s) => Proxy s -> r) -> r 
reify a f = reify' a (\(p :: Proxy s) -> case unsafeCoerce Refl :: a :~: Reflects s of Refl -> f p) 

---

Dưới đây là một phiên bản gần gũi hơn với bạn:

class Reifies s where 
    type Reflects s :: * 
    reflect :: proxy s -> Reflects s 

newtype Magic a r = Magic (forall (s :: *). (Reifies s) => Proxy s -> r) 

reify :: forall a r. a -> (forall (s :: *). (Reifies s, a ~ Reflects s) => Proxy s -> r) -> r 
reify a f = reify' a (\(p :: Proxy s) -> case unsafeCoerce Refl :: a :~: Reflects s of Refl -> f p) 
    where 
    -- This function is totally bogus in other contexts, so we hide it. 
    reify' :: forall a r. a -> (forall (s :: *). (Reifies s) => Proxy s -> r) -> r 
    reify' a k = unsafeCoerce (Magic k :: Magic a r) (const a) Proxy