Pattern Matching на продвигаемых Типы

Question

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

class MyClass d where 
    f :: d -> Int 

instance MyClass (Maybe d) where 
    f _ = 3 

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

Это компилируется нормально, и обратите внимание, что мы не нужен (MyClass (Может быть, г)) ограничение на 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 возможно) ограничение, так как компилятор находит соответствующий экземпляр.

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

{-# 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. Этот может быть связан с previous post об декомпозиции непрошеных типов. бумага по типу продвижения можно найти here.

Answer 1

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

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