断言数据构造函数是单射的

Question

我有以下数据类型:

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

然后我有一个Num实例:

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

当然这不起作用.类型a由构造函数隐藏,因为类型Var为forall (i :: Nat) a. Num a => a -> Var i.另请注意,Var构造函数不能直接使用; Vars由一个保证的智能构造函数创建Var i0 ~ Var i1 => a0 ~ a1.Var的类型不能Var i a; 重点是隐藏用户的类型.

我怎么能告诉类型系统,我已经'证明'是真实的,即那个Var i0 ~ Var i1 => a0 ~ a1.目前我正在使用unsafeCoerce:

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

我意识到这unsafeCoerce是一个断言,两个类型是相等的,但我想尝试在类型级别上进行此断言,以便导出构造函数不是不安全的.不安全我的意思是以下是可能的:

>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

一种可以说服类型系统的方法是Of :: i -> a在类型级别提供映射函数.这简单地满足了if i ~ i' => Of i ~ Of i'.这是您的程序的修改版本

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

这样做的缺点是你必须提供显式映射.可能有更优雅的方式在类型级别捕获您的约束,我等待看到更多开明的人提供洞察力.