存在类型作为返回值

Question

考虑以下数据结构,表示具有增加但不一定是连续的级别的树:

data MyTree (n :: T) where
    MyLeaf :: MyTree n
    MyNode :: Plus n m z => [MyTree ('Succ z)] -> MyTree n

其中T代表类型级别的Peano数字,定义为

class Plus (n :: T) (m :: T) (r :: T) | r n -> m
instance Plus 'Zero m m
instance Plus n m r => Plus ('Succ n) m ('Succ r)

建造树木很容易

myTreeOne :: MyTree ('Succ 'Zero)
myTreeOne = MyNode ([ MyLeaf ] :: [MyTree ('Succ ('Succ 'Zero))])

myTree :: MyTree 'Zero
myTree = MyNode [ MyLeaf, myTreeOne ]

要么

myLeafTwo :: MyTree ('Succ ('Succ 'Zero))
myLeafTwo = MyLeaf

myOtherTree :: MyTree 'Zero
myOtherTree = MyNode [ myLeafTwo ]

现在我想定义以下函数:

myTreeComponents MyLeaf              = []
myTreeComponents (MyNode components) = components

它只提取树的直接子节点列表,但我无法写出正确的类型.

这是我得到的错误

    • Couldn't match expected type ‘p’                                                                                ?
                  with actual type ‘[MyTree ('Succ z)]’                                                               ?
        because type variable ‘z’ would escape its scope                                                              ?
      This (rigid, skolem) type variable is bound by                                                                  ?
        a pattern with constructor:                                                                                   ?
          MyNode :: forall (n :: T) (m :: T) (z :: T).                                                                ?
                    Plus n m z =>                                                                                     ?
                    [MyTree ('Succ z)] -> MyTree n,                                                                   ?
        in an equation for ‘myTreeComponents’                                                                         ?
        at src/Model.hs:159:19-35                                                                                     ?
    • In the expression: components                                                                                   ?
      In an equation for ‘myTreeComponents’:                                                                          ?
          myTreeComponents (MyNode components) = components                                                           ?
    • Relevant bindings include                                                                                       ?
        components :: [MyTree ('Succ z)] (bound at src/Model.hs:159:26)                                               ?
        myTreeComponents :: MyTree n -> p (bound at src/Model.hs:158:1)                                               ?
    |                                                                                                                 ?
159 | myTreeComponents (MyNode components) = components                                                               ?
    |                                        ^^^^^^^^^^

对于依赖类型语言,它应该是类似的

exists m. Plus n m z => MyTree n -> [ MyTree ('Succ z) ]

是否可以在Haskell中编写这样的类型？否则我该怎么写我的功能？

Answer 1

这是对您的代码的修改,Proxy添加,以"记住"数字m.

{-# LANGUAGE GADTs, KindSignatures, DataKinds, TypeFamilies, 
    MultiParamTypeClasses, FunctionalDependencies,
    FlexibleInstances, UndecidableInstances #-}
{-# OPTIONS -Wall #-}

import Data.Proxy

data T = Zero | Succ T

class Plus (n :: T) (m :: T) (z :: T) | n m -> z where

instance Plus n 'Zero n
instance Plus n m z => Plus n ('Succ m) ('Succ z)

data MyTree (n :: T) where
    MyLeaf :: MyTree n
    MyNode :: Plus n m z => ! (Proxy m) -> [MyTree ('Succ z)] -> MyTree n

myTreeOne :: MyTree ('Succ 'Zero)
myTreeOne = MyNode (Proxy :: Proxy 'Zero) ([ MyLeaf ] :: [MyTree ('Succ ('Succ 'Zero))])

myTree :: MyTree 'Zero
myTree = MyNode (Proxy :: Proxy 'Zero) [ MyLeaf, myTreeOne ]

myLeafTwo :: MyTree ('Succ ('Succ 'Zero))
myLeafTwo = MyLeaf

myOtherTree :: MyTree 'Zero
myOtherTree = MyNode (Proxy :: Proxy ('Succ 'Zero)) [ myLeafTwo ]

为了能够编写最终函数myTreeComponents,我们需要一个自定义存在类型:

data Nodes (n :: T) where
    Nodes :: Plus n m z => ! (Proxy m) -> [MyTree ('Succ z)] -> Nodes n

这基本上MyTree只有第二个构造函数.最后,模式匹配现在足够了.

myTreeComponents :: MyTree n -> Nodes n
myTreeComponents MyLeaf                = Nodes (Proxy :: Proxy 'Zero) []
myTreeComponents (MyNode p components) = Nodes p components