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

【问题标题】：Generate type class constraints recursively and use them in a recursive function递归生成类型类约束并在递归函数中使用它们
【发布时间】：2021-03-16 16:26:16
【问题描述】：

我正在尝试定义一个函数，它获取一些自然数 n 作为输入。根据这个输入，函数应该有不同的约束。此约束使用类型族进行计算。该数字必须转换为GHC.TypeNats，因为约束适用于Data.Vector.Sized。我问了一个类似的问题here，但在GHC.TypeNats 和任意n 的情况下答案将不起作用。

我尝试了Clash 中的UNat 类型。

这是来自冲突的相关代码：

{-# 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
    |                ^^^^^^^

【问题讨论】：

标签： haskell

【解决方案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)

【讨论】：