Экзистенциальный тип в качестве возвращаемого значения - PullRequest
Новая
       11

Экзистенциальный тип в качестве возвращаемого значения

0 голосов
/ 15 мая 2018

Рассмотрим следующую структуру данных, представляющую дерево с уровнями, которые увеличиваются, но не обязательно являются последовательными: 

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

, где T представляет числа Пеано на уровне типа, определяемые как 

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?Иначе как мне написать свою функцию?

Ответы [ 4 ]

0 голосов
/ 16 мая 2018

Мне нравится исправление Чи, потому что использование Proxy s для хранения типов - хороший трюк под вашим поясом. В его ответе Proxy используется для устранения неоднозначности, что m использовать в ограничении Plus n m z при вызове конструктора Nodes. (На данный момент существует ограничение Plus n m z в области видимости, но без прокси-сервера нет способа указать компилятору выбрать его.)

Помимо Proxy, есть еще один способ исправить неоднозначные типы: устранить неоднозначный тип. В данном случае это m. Таким образом, вместо класса Plus n m z у нас будет класс LE n z, который имеет все те же экземпляры, но нигде не упоминает m. Итак: 

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

data T = Zero | Succ T

class LE (n :: T) (z :: T)
instance LE 'Zero n
instance LE n z => LE ('Succ n) ('Succ z)

Есть одна морщина. В ответе Чи он использует слегка измененное определение Plus, которое дает экземпляр Plus n 'Zero n бесплатно, но в вашей формулировке это недоступно, и, следовательно, LE n n не предоставляется бесплатно. Поэтому нам придется немного украсить наши листья. 

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

Все бетонные деревья такие же, как были раньше (не нужно никаких Proxy). 

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 по сравнению с ответом Чи (помимо стирания Proxy) состоит в том, что нам нужно ввести переменную типа в область видимости для использования в теле. 

data Nodes (n :: T) where
    Nodes :: LE n z => [MyTree ('Succ z)] -> Nodes n

myTreeComponents :: forall n. MyTree n -> Nodes n
myTreeComponents MyLeaf              = Nodes ([] :: [MyTree ('Succ n)])
myTreeComponents (MyNode components) = Nodes components
0 голосов
/ 15 мая 2018

Это адаптация вашего кода с добавлением 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
0 голосов
/ 16 мая 2018

Обычно вы можете использовать CPS для кодирования экзистенциалов. 

exists a. f a

можно представить как 

(forall a. f a -> r) -> r

Однако я не думаю, что ваш 

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

это тип, который вы хотите.Во-первых, существует не в том месте - не существует единого глобального типа m, но, скорее, для каждого MyTree n существует, возможно, отдельный такой m. 

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

Здесьвызывающий абонент выбирает z и, учитывая, что n + m = z, может извлечь список детей.Это соответствует, но такие доказательства могут быть трудно найти.Я думаю, что вы на самом деле хотите двойной экзистенциальный: 

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

, и я использую & в качестве двойственного к =>, тип, который поставляется со словарем, а не требует его в качестве аргумента.

type a & b = (Dict a, b)

Таким образом, для любого дерева на уровне n существует некоторое число z >= n (засвидетельствованное добавлением m), такое что список детей на уровне 'Succ z,Да, я думаю, что это правильно.Итак, теперь давайте CPS закодируем его в: 

MyTree n -> (forall m z. Plus n m z => [ MyTree ('Succ z) ] -> r) -> r
0 голосов
/ 15 мая 2018

что-то вроде (я не знаю, разрешен ли такой тип, и не могу проверить это сейчас) 

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

z тип не выставлен, поэтому он может быть любым. Если тип z был выставлен с помощью myTreeComponents, вызывающая сторона может указать для него конкретный тип, что он не должен делать

...