Сопоставление с образцом для продвигаемых типов

Мы можем написать отдельные комплексные экземпляры для параметров типа *:

class MyClass d where
    f :: d -> Int

instance MyClass (Maybe d) where  
    f _ = 3

test1 :: Maybe d -> Int
test1 x = f x

Это компилируется просто отлично, и обратите внимание, что нам НЕ нужно ограничение (MyClass (Maybe d)) для test1, потому что компилятор находит соответствующий экземпляр для любого Maybe d.

Мы даже можем написать всеобъемлющий экземпляр для параметров класса, которые являются конструкторами типов:

class MyClass2 (a :: * -> *) where
    g :: Tagged (a Int) Int

instance MyClass2 a where
    g = Tagged 3

test2 :: Int
test2 = untag (g :: Tagged (Maybe Int) Int)

Это также отлично компилируется, и test2 не нуждается в ограничении (MyClass2 Maybe), потому что компилятор находит соответствующий экземпляр.

Рассмотрим следующий игрушечный код для вычисления длины списка (продвинутых) типов:

{-# LANGUAGE TypeOperators,
DataKinds,
KindSignatures,
GADTs,
FlexibleInstances,
FlexibleContexts,
ScopedTypeVariables #-}

import Data.Tagged
import Data.Proxy

data HList :: [*] -> * where
              HNil :: HList '[]
              HCons :: a -> HList as -> HList (a ': as)

class ListLen a where
    len :: Tagged a Int

instance ListLen (HList '[]) where
    len = Tagged 0

instance (ListLen (HList as)) => ListLen (HList (a ': as)) where
    len = Tagged (1+(untag (len :: Tagged (HList as) Int)))

test3 :: Int
test3 = untag (len :: Tagged (HList '[Int, Double, Integer]) Int)

test4 :: (Proxy (HList qs)) -> Int
test4 (_ :: Proxy (HList qs)) = untag (len :: Tagged (HList qs) Int) -- error occurs here

Это приводит к ошибке:

No instance for (ListLen (HList qs))
      arising from a use of `len'
    Possible fix: add an instance declaration for (ListLen (HList qs))
    ...

Если мы закомментируем подпись для test4, GHCi выведет тип как

test4 :: (ListLen (HList qs)) => (Proxy (HList qs)) -> Int

но в этом нет необходимости. Ясно, что я написал экземпляры для ListLen, которые соответствуют любому мыслимому списку типов: случай «пустой список» и случай «против». Проблема остается той же, если я изменю тип параметра ListLen на вид [*] (т. е. удалю оболочку HList в ListLen и его экземплярах).

Если мы закомментируем test4, test3 компилируется и работает нормально: поскольку я (по сути) дал ему явный синтаксис ('[Int,Double,Integer]) для того, как я построил список типов, компилятор смог найти соответствующие экземпляры.

Я пытаюсь написать код, который создает для меня список типов, поэтому мне не придется писать явный синтаксис списка типов. Однако кажется, что использование явного синтаксиса — единственный способ, с помощью которого GHC может сопоставить эти всеобъемлющие экземпляры. Может быть, я пропустил какое-то дело? Синтаксис, который я не использую?

Что я могу сделать, чтобы GHC понял, что у меня есть экземпляр для всего вида [*]? Я использую GHC 7.4.2. Это может быть связано с предыдущим сообщением о деконструкции не продвигаемых типов. ДОКУМЕНТ о продвижении шрифтов можно найти здесь.


haskell pattern-matching higher-kinded-types type-kinds
person crockeea    schedule 13.02.2013    source источник
comment
Предложения по названию приветствуются.   -  person crockeea    schedule 13.02.2013
comment
У вас есть разные экземпляры, как бы не какой? GHC должен выбрать экземпляр, а это непараметрическая операция, поэтому требуется ограничение. Я не думаю, что то, что вы хотите сделать, имеет смысл.   -  person Philip JF    schedule 13.02.2013
comment
GHC может даже разрешать перекрывающиеся экземпляры (которыми они не являются) во время выполнения, используя явное ограничение класса (которое в противном случае было бы выведено). Почему он не видит, что соответствие всегда есть, даже если ему приходится ждать, пока время выполнения не выберет соответствующий экземпляр? Конечно, я прошу сделать это без явного (и необоснованного) ограничения класса, которое я не могу себе позволить.   -  person crockeea    schedule 13.02.2013
comment
@Eric, все экземпляры выбираются во время компиляции или передаются как параметры, сгенерированные из ограничений. Во время выполнения ничего не решается.   -  person luqui    schedule 13.02.2013
comment
@Eric: потому что экземпляры делают разные вещи. Точка в непараметричности всегда требует ограничения. Специальный полиморфизм является специальным.   -  person Philip JF    schedule 13.02.2013
comment
Попробуйте подумать об этом с точки зрения словарного перевода.   -  person Philip JF    schedule 13.02.2013

Ответы (1)


arrow_upward
2
arrow_downward

Это не совсем то, что вы хотите, но довольно близко. я начал с

data Proxy a where
  Proxy :: ListLen a => Proxy

тогда

data Proxy a where
  Proxy :: Tagged a Int -> Proxy a

в результате чего

test4 :: (Proxy (HList qs)) -> Int
test4 (Proxy len) = untag len

Проблема в том, что вам нужно либо иметь ограничение, либо Proxy содержать свидетельство требуемого класса (хотя экземпляры существуют для всех доступных типов). Здесь метод класса просто включен в Proxy.

Совсем другой вариант — просто вообще не использовать класс типов, а реализовать len обычным способом (транскрибировано из Data.List.length).

len :: HList a -> Int
len l = len' l 0
  where
    len' :: HList a -> Int -> Int
    len' HNil a = a
    len' (HCons _ xs) a = len' xs $! a + 1
person ScootyPuff    schedule 08.04.2013