如果我知道运行时是真的，该如何告诉GHC满足类型级别<=约束？

如何解决如果我知道运行时是真的，该如何告诉GHC满足类型级别<=约束？

我有一个由自然数n参数化的类型：

data MyType (n :: Nat) = MyType

这种类型的操作仅在n > 0时才有意义，因此我将其指定为约束：

myFunction :: (KnownNat n,1 <= n) => MyType n -> MyType n
myFunction = id

（请注意，这些功能的实际版本 do 通过将n转换为natVal来使用SomeMyType。）

我想创建一个存在性类型（n），让我们在运行时选择一个data SomeMyType where SomeMyType :: forall n. (KnownNat n,1 <= n) => MyType n -> SomeMyType ：

SomeMyType

要产生someMyTypeVal的值，我正在编写一个someNatVal的函数，其作用类似于someMyTypeVal :: Integer -> Maybe SomeMyType someMyTypeVal n | n > 0 = case someNatVal n of Just (SomeNat (_ :: p n)) -> Just (SomeMyType (MyType @n)) Nothing -> Nothing | otherwise = Nothing ：

1 <= n

这在没有• Couldn't match type ‘1 <=? n’ with ‘'True’ arising from a use of ‘SomeMyType’ 约束的情况下可以很好地工作，但是在约束条件下，我收到以下类型错误：

n > 0

如何解决此限制？由于我在运行时检查过unsafeCoerce，因此我不介意在此处使用类似1 <= n的操作来说服GHC unsafeCoerce是正确的，但我不能 just 使用n，因为那样会丢失<layout xmlns:android="http://schemas.android.com/apk/res/android" xmlns:app="http://schemas.android.com/apk/res-auto"> <androidx.drawerlayout.widget.DrawerLayout android:id="@+id/drawerLayout" android:layout_width="match_parent" android:layout_height="match_parent" > <LinearLayout android:layout_width="match_parent" android:layout_height="match_parent" android:orientation="vertical"> <fragment android:id="@+id/myNavHostFragment" android:name="androidx.navigation.fragment.NavHostFragment" android:layout_width="match_parent" android:layout_height="match_parent" app:defaultNavHost="true" app:navGraph="@navigation/navigation" /> </LinearLayout> <com.google.android.material.navigation.NavigationView android:id="@+id/navView" android:layout_width="wrap_content" android:layout_height="match_parent" android:layout_gravity="start" app:menu="@menu/navdrawer_menu" app:headerLayout="@layout/nav_header"/> </androidx.drawerlayout.widget.DrawerLayout> 的类型级别的值。

处理此问题的最佳方法是什么？

解决方法

经过一番摸索，我发现了Justin L's answer to a similar question。他将解决方案包装到typelits-witnesses程序包中，我可以使用它很干净地解决此问题：

someMyTypeVal :: Integer -> Maybe SomeMyType
someMyTypeVal n = someNatVal n >>= check
  where check :: SomeNat -> Maybe SomeMyType
        check (SomeNat (_ :: p n)) = case (SNat @1) %<=? (SNat @n) of
          LE Refl -> Just (SomeMyType (MyType @n))
          NLE _ _ -> Nothing

a %<=? b让我们比较两个类型级别的自然数，并为我们证明a是否小于b（LE）（{{1 }}。这在NLE情况下给了我们额外的约束，以返回LE，但是在SomeMyType情况下尝试这样做仍然会给我们“无法匹配'1

请注意NLE的显式类型签名-如果没有显式类型签名，则将check的类型推断为check，我将收到以下类型错误：

check :: SomeNat -> Maybe a

使用显式类型签名，一切正常，并且代码甚至（合理地）可读。

,

作为更直接的答案，约束1 <= n只是1 <=? n ~ 'True的类型别名。您可以使用以下方法不安全地创建这样的类型相等约束：

{-# LANGUAGE DataKinds,TypeOperators #-}

import Data.Type.Equality
import GHC.TypeLits
import Unsafe.Coerce

unsafeDeclarePositive :: p n -> (1 <=? n) :~: 'True
unsafeDeclarePositive _ = unsafeCoerce Refl

这或多或少是typelits-witnesses在幕后所做的事情。

有了该定义，以下内容应进行类型检查：

someMyTypeVal :: Integer -> Maybe SomeMyType
someMyTypeVal n
  | n > 0 = case someNatVal n of
      Just (SomeNat (pxy :: p n)) ->
        case unsafeDeclarePositive pxy of
          Refl -> Just (SomeMyType (MyType @n))
      Nothing -> Nothing
  | otherwise = Nothing