haskell - 递归生成类型类约束并在递归函数中使用它们

Question

我正在尝试定义一个函数来获取一些自然数 n作为输入。根据这个输入，函数应该有不同的约束。此约束使用类型系列进行计算。该数字必须转换为 GHC.TypeNats因为约束是针对 Data.Vector.Sized .我问了一个类似的问题 here ，但答案在 GHC.TypeNats 的情况下不起作用和任意n .
我试过 UNat输入来自 Clash .
这是来自冲突的相关代码:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}

{-# LANGUAGE Trustworthy #-}

{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise       #-}


import GHC.TypeNats
import GHC.Natural

import Unsafe.Coerce      (unsafeCoerce)
import Data.Kind (Constraint)

data SNat (n :: Nat) where
  SNat :: KnownNat n => SNat n

data UNat :: Nat -> * where
  UZero :: UNat 0
  USucc :: UNat n -> UNat (n + 1)

snatToInteger :: SNat n -> Natural
snatToInteger p@SNat = natVal p

toUNat :: forall n. SNat n -> UNat n
toUNat p@SNat = fromI @n (snatToInteger p)
  where
    fromI :: forall m. Natural -> UNat m
    fromI 0 = unsafeCoerce @(UNat 0) @(UNat m) UZero
    fromI n = unsafeCoerce @(UNat ((m-1)+1)) @(UNat m) (USucc (fromI @(m-1) (n - 1)))

这解决了递归问题，但不能解决约束问题。
这是一个最小的例子:

type family F (m :: Nat) (n :: Nat) :: Constraint where
  F m 0 = ()
  F m n = ((0 <=? m) ~ 'True, F m (n - 1))

fU :: forall m n. (KnownNat m, KnownNat n, F m n) => UNat n -> ()
fU UZero = ()
fU (USucc s) = fU @m s

这会返回错误:

• Could not deduce: F m n1 arising from a use of ‘fU’
      from the context: (KnownNat m, KnownNat n, F m n)
        bound by the type signature for:
                   fU :: forall (m :: Nat) (n :: Nat).
                         (KnownNat m, KnownNat n, F m n) =>
                         UNat n -> ()
        at src-lib/Anomaly/NeuralNetworks/Peano.hs:103:1-65
      or from: n ~ (n1 + 1)
        bound by a pattern with constructor:
                   USucc :: forall (n :: Nat). UNat n -> UNat (n + 1),
                 in an equation for ‘fU’
        at src-lib/Anomaly/NeuralNetworks/Peano.hs:105:5-11
    • In the expression: fU @m s
      In an equation for ‘fU’: fU (USucc s) = fU @m s
    • Relevant bindings include
        s :: UNat n1
          (bound at src-lib/Anomaly/NeuralNetworks/Peano.hs:105:11)
    |
105 | fU (USucc s) = fU @m s
    |                ^^^^^^^

Answer 1

我通过向 GADT Peano nat 的构造函数添加约束来解决这个问题。

data CNat :: Nat -> Nat -> * where
  CZero :: forall n m. CNat 0 m
  CSucc :: forall n m. (0 <=? m) ~ 'True => CNat n m -> CNat (n + 1) m

fC :: forall n m. (KnownNat n, KnownNat m) => CNat n m -> ()
fC CZero = ()
fC (CSucc s) = fC s

这是一个示例，它表明条件在第二个模式中确实成立。

hC :: forall m. ((0 <=? m) ~ 'True) => ()
hC = ()

gC :: forall n m. CNat n m -> () -> ()
gC CZero _ = ()
gC (CSucc s) _ = gC s (hC @m)