主页 / coding / 问题 / 79565069
Accepted
Ashok Kimmel
Asked: 2025-04-10 02:25:26 +0800 CST

使用自然类型的非法函数依赖，

  • 772
data Zero = Zero 
data Succ x = Succ x 

class NatToPeano a b | a -> b where 
    toPean :: b
instance NatToPeano 0 Zero where toPean = Zero 
instance (NatToPeano (x-1) a) => NatToPeano x (Succ a) where
     toPean = Succ (toPean @(x-1))

这会产生错误：

 Functional dependencies conflict between instance declarations:
  instance NatToPeano 0 Zero -- Defined at parsejava.hs:26:10
  instance NatToPeano (x - 1) a => NatToPeano x (Succ a)
    -- Defined at parsejava.hs:28:10

 26 | instance NatToPeano 0 Zero where
haskell

2 个回答

  1. Best Answer

    根据@Noughtmare的回答，您可能无法完全按照此处的说明进行操作。要获得在GHC类型级自然数和类型级皮亚诺数之间来回转换的全面解决方案，请考虑使用type-natural包，该包使用了许多技巧来确保正确执行此操作，并提供适当的机制使其真正可用。

    使用当前代码，您可能能够想到的最接近的方法是定义一个类型系列，以仅在类型级别将 GHC 类型级自然数转换为 Peano 表示：

    type family ToPeano n where
  ToPeano 0 = Zero
  ToPeano n = Succ (ToPeano (n-1))

    然后引入一个类来从其类型生成项级皮亚诺数：

    class KnownPeano p where
  peano :: p
instance KnownPeano Zero where peano = Zero
instance KnownPeano x => KnownPeano (Succ x) where peano = Succ peano

    这将允许您定义一个函数：

    toPeano :: (KnownPeano (ToPeano n)) => ToPeano n
toPeano = peano

    它使用ToPeano类型族从 GHC 自然数中计算出适当的 Peano 类型，然后使用peano类型类函数为 Peano 类型生成术语级 Peano 值，因此你可以这样写：

    ghci> toPeano @0
Zero
ghci> toPeano @2
Succ (Succ Zero)

    这可能是您想要的，但很难说它是否真的会在您的实际应用中发挥作用。

    完整代码：

    {-# LANGUAGE GHC2021 #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module FundepPeano where

import GHC.TypeNats

data Zero = Zero
  deriving (Show)
data Succ x = Succ x
  deriving (Show)

type family ToPeano n where
  ToPeano 0 = Zero
  ToPeano n = Succ (ToPeano (n-1))

class KnownPeano p where
  peano :: p
instance KnownPeano Zero where peano = Zero
instance KnownPeano x => KnownPeano (Succ x) where peano = Succ peano

toPeano :: (KnownPeano (ToPeano n)) => ToPeano n
toPeano = peano

main :: IO ()
main = do
  print $ toPeano @0
  print $ toPeano @2
    • 3

  2. 你有两个实例，一个是“说” NatToPeano 0 Zero，另一个是“包含” NatToPeano 0 (Succ a)（带有一些约束）。我认为类型类实例解析和函数依赖关系检查没有考虑到这些约束，所以这会产生冲突。

    • 2

相关问题