时间戳

首页 > 解决方案 > 规范化 TypeNats 不等式

haskell - 规范化 TypeNats 不等式

问题描述

我有两个具有 Nat（来自 TypeNats）类型的函数，它们都有一个比较类型 operator <=。2 <= nfunction的约束b包含 function 的1 <= n约束a。有没有办法让 ghc 解决2 <= n满足约束1 <= n的问题，这样我就不必为 指定两个(1 <= n, 2 <= n)约束b？

下面的代码演示了错误。

{-# LANGUAGE KindSignatures, TypeOperators, ScopedTypeVariables, 
             DataKinds, TypeFamilies #-}

import GHC.TypeNats
import Data.Proxy

a :: forall (a :: Nat). 1 <= a => Proxy a -> Int
a = undefined

b :: forall (a :: Nat). 2 <= a => Proxy a -> Int
b = a

导致编译错误

• Could not deduce: (1 <=? a) ~ 'True arising from a use of ‘a’
  from the context: 2 <= a
    bound by the type signature for:
               b :: forall (a :: Nat). (2 <= a) => Proxy a -> Int
    at Example.hs:9:1-48
• In the expression: a
  In an equation for ‘b’: b = a
• Relevant bindings include
    b :: Proxy a -> Int
      (bound at Example.hs:10:1)

有一个库可以解决等式 ghc-typelits-natnormalise但不是不等式。

标签： haskelltypesdata-kinds

解决方案

尽管有包描述，但ghc-typelits-natnormalise也可以解决不等式。以下程序类型检查与 GHC 8.6.4 和ghc-typelits-natnormalise-0.6.2：

{-# LANGUAGE KindSignatures, TypeOperators, ScopedTypeVariables,
             DataKinds, TypeFamilies #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise -Wall #-}

import GHC.TypeNats
import Data.Proxy

a :: forall (a :: Nat). 1 <= a => Proxy a -> Int
a = undefined

b :: forall (a :: Nat). 2 <= a => Proxy a -> Int
b = a

推荐阅读