尽管明确注释,Haskell无法推断类型(或类型级别Nat)的等式？

2023年12月7日 295次阅读

我试图用
Haskell实现一个Braun Tree,定义如下：

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}

data BraunTree (n :: Nat) a where
    Empty :: BraunTree 0 a
    Fork :: a -> BraunTree n a -> 
            BraunTree m a ->
            Either (n :~: m) (n :~: (m + 1)) ->
            BraunTree (n + m + 1) a

现在,我试图尝试如何“类型安全地”将东西插入到这棵树中.

insert :: a -> BraunTree (n :: Nat) a -> BraunTree (n + 1 :: Nat) a
insert x Empty = Fork x Empty Empty (Left Refl)
insert x (Fork y (t1 :: BraunTree p a) (t2 :: BraunTree q a) (Left (Refl :: p :~: q))) = Fork x (t1' :: BraunTree (p + 1) a) (t2 :: BraunTree q a) (Right (sucCong Refl :: (p + 1) :~: (q + 1)))
    where
        t1' :: BraunTree (p + 1) a
        t1' = insert x t1

与sucCong一样

sucCong :: ((p :: Nat) :~: (q :: Nat)) -> (p + 1 :: Nat) :~: (q + 1 :: Nat)
sucCong Refl = Refl

现在,虽然插入的第一个子句编译得很好,但第二行会引发一个令人困惑的错误.

/home/agnishom/test/typeExp/braun.hs:31:90: error:
    • Could not deduce: (((n1 + 1) + n1) + 1) ~ (n + 1)
      from the context: n ~ ((n1 + m) + 1)
        bound by a pattern with constructor:
                   Fork :: forall a (n :: Nat) (m :: Nat).
                           a
                           -> BraunTree n a
                           -> BraunTree m a
                           -> Either (n :~: m) (n :~: (m + 1))
                           -> BraunTree ((n + m) + 1) a,
                 in an equation for ‘insert’
        at /home/agnishom/test/typeExp/braun.hs:31:11-85
      or from: m ~ n1
        bound by a pattern with constructor:
                   Refl :: forall k (a :: k). a :~: a,
                 in an equation for ‘insert’
        at /home/agnishom/test/typeExp/braun.hs:31:69-72
      Expected type: BraunTree (n + 1) a
        Actual type: BraunTree (((n1 + 1) + m) + 1) a
      NB: ‘+’ is a type function, and may not be injective
    • In the expression:
        Fork
          x
          (t1' :: BraunTree (p + 1) a)
          (t2 :: BraunTree q a)
          (Right (sucCong Refl :: (p + 1) :~: (q + 1)))
      In an equation for ‘insert’:
          insert
            x
            (Fork y
                  (t1 :: BraunTree p a)
                  (t2 :: BraunTree q a)
                  (Left (Refl :: p :~: q)))
            = Fork
                x
                (t1' :: BraunTree (p + 1) a)
                (t2 :: BraunTree q a)
                (Right (sucCong Refl :: (p + 1) :~: (q + 1)))
            where
                t1' :: BraunTree (p + 1) a
                t1' = insert x (t1 :: BraunTree p a)
    • Relevant bindings include
        t1' :: BraunTree (n1 + 1) a
          (bound at /home/agnishom/test/typeExp/braun.hs:34:9)
        t1 :: BraunTree n1 a
          (bound at /home/agnishom/test/typeExp/braun.hs:31:19)
        insert :: a -> BraunTree n a -> BraunTree (n + 1) a
          (bound at /home/agnishom/test/typeExp/braun.hs:29:1)

我不确定我在这里做错了什么.另外,为什么haskell认为t1 :: BraunTree n1 a(在错误消息中),即使我注释了t1 :: BraunTree p a？

帮助解释此错误消息将非常有帮助

最佳答案 您可以尝试使用此编译器插件,它会自动为您推断Nats的类型等式：

> https://github.com/clash-lang/ghc-typelits-natnormalise

点赞