Haskell 简化依赖类型函数签名

Question

这是依赖类型 haskell 函数的示例dfunc。它的类型取决于参数值：零映射到值，Int一映射到值，Integer依此类推，如下面的类型族中所定义。

所以我有带有dfunc签名的函数GADTInt a -> Dt a 但是我想摆脱这种奇怪的GADTInt aint 编码并实现带有类型签名的函数Int -> Dt a我知道a类型对于这个来说是通用的..，但我尝试用typeclass NTI没有ff类型签名的函数来欺骗，让 haskell 为我进行类型推断，并得到错误，据我所知，因为ff实现在类型签名中无法表达。

我可以在这里做一些“魔法”来摆脱GADTInt a -> Dt a它并用它代替吗Int -> ?

{-# LANGUAGE DataKinds      #-}
{-# LANGUAGE GADTs          #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
module Main where


data Nat :: * where
    Z :: Nat
    S :: Nat -> Nat


data GADTInt a where
    GADTZero :: GADTInt Z
    GADTOne :: GADTInt (S Z)
    GADTTwo :: GADTInt (S (S Z))   
    GADTThree :: GADTInt (S (S (S Z)))   

type family Dt a where
    Dt 'Z = Int
    Dt ('S 'Z) = Integer
    Dt ('S ('S 'Z)) = Float
    Dt ('S ('S ('S 'Z))) = String

class NTI a where
    toi :: a -> Int

instance NTI (GADTInt a) where
    toi GADTZero = 0 
    toi GADTOne = 1 
    toi GADTTwo = 2
    toi GADTThree = 3

dfunc :: GADTInt a -> Dt a
dfunc GADTZero = 1
dfunc GADTOne = 1000000000000000000000000000000
dfunc GADTTwo = 3.14
dfunc GADTThree = "Hi"

ff i 
     | toi GADTZero == i = dfunc GADTZero     
     | toi GADTOne == i = dfunc GADTOne
     | toi GADTTwo == i = dfunc GADTTwo     
     | toi GADTThree == i = dfunc GADTThree
     | otherwise = undefined

Answer 1

使用 a 的唯一方法Dt a是知道a是什么。因为类型被删除，所以您将需要它的运行时表示，例如使用GADTInt单例。您可以将它们打包为存在类型：

data SomeDt where
  SomeDt :: GADTInt a -> Dt a -> SomeDt

将单例包装在另一种存在类型中也很有用：

data SomeGADTInt where
  SomeGADTInt :: GADTInt a -> SomeGADTInt

这样您就可以定义“非依赖”标记：

toTag :: Int -> SomeGADTInt
toTag 0 = SomeGADTInt GADTZero
toTag 1 = SomeGADTInt GADTOne
toTag 2 = SomeGADTInt GADTTwo
toTag 3 = SomeGADTInt GADTThree

裹dfunc：

someDFunc :: SomeGADTInt -> SomeDt
someDFunc (SomeGADTInt i) = SomeDt i (dfunc i)

撰写：

ff :: Int -> SomeDt
ff = someDFunc . toTag