Início / coding / Perguntas / 79565069
Accepted
Ashok Kimmel
Asked: 2025-04-10 02:25:26 +0800 CST

Dependências funcionais ilegais usando o tipo natural,

  • 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))

Isso produz o erro:

 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 respostas

  1. Best Answer

    Conforme a resposta de @Noughtmare, você provavelmente não consegue fazer exatamente o que está tentando fazer aqui. Para uma solução abrangente para a conversão entre números naturais de nível de tipo GHC e números Peano de nível de tipo, considere o pacote type-natural , que utiliza muitos truques para acertar isso e fornecer o maquinário apropriado para torná-lo realmente utilizável.

    O mais próximo que você pode chegar com seu código atual é definir uma família de tipos para converter os tipos naturais do GHC em sua representação Peano somente no nível de tipo:

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

    e então introduzir uma classe para gerar números Peano de nível de termo a partir de seu tipo:

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

    Isso permitirá que você defina uma função:

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

    que usa a ToPeanofamília de tipos para calcular o tipo Peano apropriado a partir do GHC natural e, em seguida, a peanofunção de classe de tipo para gerar o valor Peano de nível de termo para o tipo Peano, então você pode escrever:

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

    Isso pode ser o que você queria, mas é difícil dizer se realmente funcionará na sua aplicação real.

    O código completo:

    {-# 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. Você tem duas instâncias, uma diz NatToPeano 0 Zeroe a outra inclui NatToPeano 0 (Succ a)(com algumas restrições). A resolução de instâncias de classe de tipo e acredito que a verificação de dependência funcional não leva as restrições em consideração, então isso é um conflito.

    • 2

relate perguntas