twierdzą, że konstruktor danych jest injective

Question

Mam następujący typ danych:

{-# LANGUAGE GADTs, KindSignatures, ScopedTypeVariables, DataKinds #-} 

import GHC.TypeLits 
import Unsafe.Coerce 

data Var (i :: Nat) where 
    Var :: (Num a, Integral a) => a -> Var i 
    {- other constructors .... -} 

to mam instancję Num:

instance Num (Var i) where 
    (Var a) + (Var b) = Var (a + b) 

Oczywiście to nie zadziała. Typ a jest ukryty przez konstruktora, ponieważ typ Var to forall (i :: Nat) a. Num a => a -> Var i. Należy również zauważyć, że konstruktor Var nie jest przeznaczony do bezpośredniego użycia; Var s są tworzone przez inteligentnego konstruktora, który gwarantuje Var i0 ~ Var i1 => a0 ~ a1. Typ Var nie może być Var i a; chodzi o to, aby ukryć typ przed użytkownikiem.

Jak mogę powiedzieć systemowi, co "sprawdziłem", że jest prawdziwe, a mianowicie, że Var i0 ~ Var i1 => a0 ~ a1. Obecnie używam unsafeCoerce:

(Var (a :: n)) + (Var b) = Var (a + (unsafeCoerce b :: n)) 

Zdaję sobie sprawę, że unsafeCoerce jest w twierdzeniu, że dwa typy są równe, ale chciałbym spróbować zrobić to twierdzenie na poziomie typu, dzięki czemu eksportu ISN konstruktora” t niebezpieczne. Przez niebezpieczne Znaczy następuje to możliwe:

>instance Show (Var i) where {show (Var a) = "Var " ++ show a} 
>import Data.Word 
>Var (1000 :: Word16) + Var (255 :: Word8) 
Var 1255 
>Var (255 :: Word8) + Var (1000 :: Word16) 
Var 231 

Answer 1

Możliwym sposobem można przekonać system typów jest realizowanie funkcji mapowania Of :: i -> a na poziomie typu. To banalnie spełnia, że ​​jeśli i ~ i' => Of i ~ Of i'. Oto zmodyfikowana wersja programu

{-# LANGUAGE GADTs, KindSignatures, ScopedTypeVariables, DataKinds, TypeFamilies, FlexibleContexts #-} 

import GHC.TypeLits 
import Unsafe.Coerce 

type family Of :: Nat -> * 

data Var (i :: Nat) where 
    Var :: (Num (Of i), Integral (Of i)) => (Of i) -> Var i 

instance Num (Var i) where 
    (Var a) + (Var b) = Var (a + b) 

Wadą jest to, że musisz podać wyraźne odwzorowanie. Może być bardziej elegancki sposób uchwycenia twojego ograniczenia na poziomie typu i czekam, aby zobaczyć więcej oświeconych ludzi dających wgląd w to.