如何满足对存在量化价值的约束？

Question

为了学习如何在haskell中使用依赖数据类型，我遇到了以下问题：

假设您有一个函数，如：

mean :: ((1 GHC.TypeLits.<=? n) ~ 'True, GHC.TypeLits.KnownNat n) => R n -> ℝ

在hmatrix库中定义，那么如何在具有存在类型的向量上使用？例如：

{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators       #-}

import Data.Proxy                   (Proxy (..))
import GHC.TypeLits
import Numeric.LinearAlgebra.Static

getUserInput =
  let userInput = 3   -- pretend it's unknown at compile time
      seed      = 42
  in existentialCrisis seed userInput

existentialCrisis seed userInput
  | userInput <= 0 = 0
  | otherwise =
    case someNatVal userInput of
      Nothing -> undefined -- let's ignore this case for now
      Just (SomeNat (proxy :: Proxy n)) ->
        let someVector = randomVector seed Gaussian :: R n
        in mean someVector -- I know that 'n > 0' but the compiler doesn't

这会产生以下错误：

• Couldn't match type ‘1 <=? n’ with ‘'True’
    arising from a use of ‘mean’

确实很有道理，但在谷歌和兜圈子之后，我无法找到如何处理这个问题。如何根据用户输入获得n :: Nat，使其满足1 <= n约束？我相信这是可能的，因为基于输入不是负的条件，someNatVal函数已经成功地满足了KnownNat约束。

在我看来，在处理依赖类型时，这是一件常见的事情，也许答案是显而易见的，但我没有看到。

所以我的问题是：

一般情况下，我如何才能在范围内引入满足某种函数所需约束的存在类型？

我的尝试：

• 令我惊讶的是，即使是下面的修改 设someVector = randomVector种子高斯:：r (n + 1) 给出一个类型错误： ·无法与‘1型<=相匹配？(n +1)加上“真”，因使用“平均数”而产生 另外，在<=?中添加一个额外的实例来证明这个等式在关闭<=?时是不起作用的。
• 我尝试了一种将GADTs与类型化相结合的方法，比如在对我先前的一个问题的回答中，但无法使其工作。

Answer 1

谢谢@danidiaz为我指明了正确的方向，typelist-witnesses文档为我的问题提供了一个几乎直接回答。似乎我在谷歌搜索解决方案时使用了错误的搜索词。

下面是一个自成体系的可编译解决方案：

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

import Data.Proxy                   (Proxy (..))
import Data.Type.Equality           ((:~:)(Refl))
import GHC.TypeLits
import GHC.TypeLits.Compare
import Numeric.LinearAlgebra.Static

existentialCrisis :: Int -> Int -> IO (Double)
existentialCrisis seed userInput =
    case someNatVal (fromIntegral userInput) of
      Nothing -> print "someNatVal failed" >> return 0
      Just (SomeNat (proxy :: Proxy n)) ->
        case isLE (Proxy :: Proxy 1) proxy of
          Nothing -> print "isLE failed" >> return 0
          Just Refl ->
            let someVector = randomVector seed Gaussian :: R n
            in do
              print userInput
              -- I know that 'n > 0' and so does the compiler
              return (mean someVector)

它只在运行时使用已知的输入：

λ: :l ExistentialCrisis.hs 
λ: existentialCrisis 41 1
(0.2596687587224799 :: R 1)
0.2596687587224799
*Main
λ: existentialCrisis 41 0
"isLE failed"
0.0
*Main
λ: existentialCrisis 41 (-1)
"someNatVal failed"
0.0

看起来typelist-witnesses在引擎盖下做了很多unsafeCoerce工作。但是接口是类型安全的，所以对于实际用例来说并不重要。

编辑：

如果你对这个问题感兴趣，你可能也会发现这个帖子很有趣：https://stackoverflow.com/a/41615278/2496293