haskell - 在编译时生成类型级别 Nats 进行约束检查

Question

我试图在编译时在类型级别表示整数值，以便我可以根据某些约束对其进行检查。

我希望 DSL 的用户不必编写如下内容:

five = inc $ inc $ inc $ inc $ inc $ zero

因此，我一直在尝试创建一个将该值提升到类型级别的函数。

即

fromInt :: Int -> repr n
fromInt n = __

这是我迄今为止尝试过的:

data Z
data S a

data IntNat a = IN Int

zero = (IN 0 :: IntNat Z)

inc :: IntNat a -> IntNat (S a)
inc (IN i) = (IN (i + 1))

fromInt :: Int -> IntNat a 
fromInt 0 = (IN 0 :: IntNat Z)
fromInt n = inc (fromInt (n - 1))

然而，由于我没有足够通用的 IntNat 表示，所以这会失败，IntNat Z ~/~ IntNat S Z。

这种方法通常存在缺陷，还是需要将 S Z 包含在类型族/类型类中？

另一个经典示例是在使用类型级别长度注释向量时生成特定长度的向量。该函数应该可以解决我遇到的相同问题。

Answer 1

由于 Haskell 没有依赖类型，因此无法将值级别 Int 提升为类型级别自然值。根据您的用例，您有几个近似选项。

使用连续传递样式

{-# LANGUAGE Rank2Types #-}

fromInt :: Int -> (forall a. IntNat a -> r) -> r
fromInt 0 f = f zero
fromInt n f = fromInt (n - 1) (f . inc)

使用存在类型

{-# LANGUAGE ExistentialQuantification #-}

data AnyIntNat = forall n. AnyIntNat (IntNat n)

fromInt :: Int -> AnyIntNat
fromInt 0 = AnyIntNat zero
fromInt n =
  case fromInt (n - 1) of
    AnyIntNat m -> AnyIntNat (inc m)

利用现有的类型级文字

{-# LANGUAGE AllowAmbiguousTypes, DataKinds, FlexibleContexts,
  TypeApplications, TypeFamilies, TypeOperators, UndecidableInstances
  #-}

import GHC.TypeLits

class GetIntNat n where
  getIntNat :: IntNat n

instance GetIntNat Z where
  getIntNat = zero

instance GetIntNat n => GetIntNat (S n) where
  getIntNat = inc getIntNat

type family Peano n where
  Peano 0 = Z
  Peano n = S (Peano (n - 1))

-- usage: fromNat @5
fromNat :: GetIntNat (Peano n) => IntNat (Peano n)
fromNat = getIntNat