8

我有以下数据类型：

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

1 回答 1

5

您可以说服类型系统的一种可能方法是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)

这样做的缺点是您必须提供显式映射。可能有更优雅的方法可以在类型级别捕获您的约束，我正在等待看到更多开明的人对此提供见解。

于 2013-10-18T07:19:48.833 回答