affermano che un costruttore di dati è iniettiva

Question

Ho il seguente tipo di dati:

{-# 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 .... -} 

poi ho un esempio Num:

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

Naturalmente questo non funziona. Il tipo a è nascosto dal costruttore, perché il tipo di Var è forall (i :: Nat) a. Num a => a -> Var i. Si noti inoltre, il costruttore Var non è destinato ad essere utilizzato direttamente; Var s sono creati da un costruttore intelligente che garantisce Var i0 ~ Var i1 => a0 ~ a1. Il tipo di Var non può essere Var i a; il punto è nascondere il tipo dall'utente.

Come posso dire al sistema di tipo, quello che ho 'provata' per essere vero, e cioè che Var i0 ~ Var i1 => a0 ~ a1. Attualmente sto usando unsafeCoerce:

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

mi rendo conto che unsafeCoerce è in un'affermazione che due tipi sono uguali, ma vorrei cercare di fare questa affermazione a livello tipo, in modo che l'esportazione del costruttore isn' t pericoloso. Con pericoloso intendo la seguente è possibile:

>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

Un modo possibile è possibile convincere il sistema dei tipi è fornendo la funzione di mappatura Of :: i -> a a livello tipo. Questo soddisfa banalmente questo se i ~ i' => Of i ~ Of i'. Ecco la versione modificata del programma

{-# 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) 

Lo svantaggio di questo è che bisogna fornire la mappatura esplicita. Ci potrebbe essere più elegante modo di catturare il vostro vincolo a livello di tipo e sono in attesa di vedere le persone più illuminate dare una visione in quello.