Экземпляр IsList для GADT - PullRequest
Новая
       55

Экземпляр IsList для GADT

0 голосов
/ 03 июня 2018

У меня проблемы с реализацией IsList экземпляра для GADT, который представляет структуру значений во вложенных массивах.Вот полный код: 

{-# LANGUAGE DataKinds         #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs             #-}
{-# LANGUAGE RankNTypes        #-}
{-# LANGUAGE TypeFamilies      #-}

import GHC.Exts (IsList (..))

data ValType = TInt | TList

data Val (t :: ValType) where
    I :: Int -> Val 'TInt
    L :: [Val a] -> Val 'TList

instance Show (Val t) where
  show (I i) = "I " ++ show i
  show (L a) = show a

instance IsList (Val 'TList) where
    type Item (Val 'TList) = forall a . Val a

    fromList = L
    toList = error "Not implemented!"

Я вижу такую ​​ошибку: 

GADT.hs:20:10: error:
    • Illegal polymorphic type: forall (a :: ValType). Val a
    • In the type instance declaration for ‘Item’
      In the instance declaration for ‘IsList (Val  'TList)’
   |
20 |     type Item (Val 'TList) = forall a . Val a
   |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Я частично понимаю, почему у меня есть эта ошибка.Но я хотел бы знать, возможно ли реализовать экземпляр IsList для типа Val?

Ответы [ 2 ]

0 голосов
/ 04 июня 2018

Вы выбрасываете информацию, сохраняя только тот факт, что L ... содержит список Val a s в своем типе.Если вы храните эту информацию около 

data ValType = TInt | TList ValType

data Val (t :: ValType) where
    I :: Int     -> Val 'TInt
    L :: [Val a] -> Val ('TList a)

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

instance IsList (Val ('TList a)) where
    type Item (Val ('TList a)) = Val a

    fromList      = L
    toList (L xs) = xs

-- (For completeness, this example requires the OverloadedLists extension)
example :: String
example = show ([I 1, I 2, I 3] :: Val ('TList TInt))

Также обратите внимание, что вы можете реализоватьtoList.Поскольку этот toList имеет тип Val ('TList a) -> [Val a], он не может быть передан не в списке, поэтому приведенная выше реализация не является частичной.Вы можете проверить этот тип самостоятельно, используя отверстие типа: toList = _.Вы также можете проверить, что реализация (попытка), подобная следующей, приведет к ошибке типа: toList (I x) = undefined.

Каждый элемент в списке должен иметь один и тот же тип (нельзя смешивать целые числа со списками внутриодин список, например), но это также относится к исходному коду из вопроса.

0 голосов
/ 03 июня 2018

IsList не подходит для этого, поскольку тип элемента Item l должен определяться типом списка l.Однако перегрузка списков может быть продолжена с помощью RebindableSyntax: 

{-# LANGUAGE RebindableSyntax, OverloadedLists #-}

fromListN :: _Int -> [Val a] -> Val 'TList
fromListN _ = L

Теперь [[I 3, I 2]] - это сахар для fromListN 1 [fromListN 2 [I 3, I 2]], который уменьшается до L [L [I 3, I 2]].

Мы можем сохранитьисходное поведение с использованием класса типов, например IsList, но который разделяет элементы и типы списков. 

class IsList item l where
  fromListN :: Int -> [item] -> l

instance IsList (Val a) (Val 'TList) where
  fromListN _ = L

instance (item ~ item') => IsList item [item'] where
  fromListN _ = id
...