问题

以下是翻译好的部分：

This is an example of dependent type haskell function dfunc. Its type depends on the argument value: zero maps to value of Int one maps to value of Integer and so on as defined in type family below.

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

So I have function dfunc with signature GADTInt a -> Dt a
But I want to get rid of this wierd GADTInt a encoding of int and implement a function with type signature Int -> Dt a I understand that a type is too generic for this.., but I try to cheat with typeclass NTI and function ff without type signature, to let haskell do type inference for me, and get error, as i understand because ff implementation inexpressible in a type signature.

因此，我有一个带有签名 GADTInt a -> Dt a 的函数 dfunc，但我想摆脱这种奇怪的 GADTInt a 对整数的编码，并实现带有类型签名 Int -> Dt a 的函数。我理解 a 类型对于这个目标来说太通用了...但我尝试通过使用 typeclass NTI 和没有类型签名的函数 ff 来欺骗 Haskell 让它为我进行类型推断，结果出现错误，我明白这是因为 ff 的实现在类型签名中无法表达。

Can I do some "magic" here to get rid of GADTInt a -> Dt a and replace it with Int -> ?

我能否在这里进行一些“魔法”来摆脱 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

答案1

得分: 5

使用 `Dt a` 的唯一方式是知道 `a` 的具体类型。因为类型信息在运行时会被擦除，你需要一种运行时的表示方法，例如使用 `GADTInt` 单例类型。你可以将它们封装在一个存在类型中：

```haskell
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

<details>
<summary>英文:</summary>

The only way to use a `Dt a` is to know what `a` is. Because types are erased, you will need a run-time representation of it, for example using the `GADTInt` singleton. You can package those in an existential type:

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

It's also useful to wrap the singleton in another existential type:

data SomeGADTInt where
SomeGADTInt :: GADTInt a -> SomeGADTInt

so that you can define the "non-dependent" tagging:

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

wrap `dfunc`:

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

compose:

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

</details>