Как установить порядок между типами в Haskell

Мне нужно установить порядок между * -> * типами на основе того, что каждый член одного типа может быть представлен другим. Это гомоморфизм.

Проблема в том, что я могу определить транзитивность отношения !<=!, но программа проверки типов не может этого понять. Это также очень неоднозначно, Identity !<=! Maybe может быть получено из Identity !<=! Maybe или Identity !<=! Identity !<=! Maybe, ... Каждое производное имеет другое (но эквивалентное) определение для repr.

Поэтому я ищу другие способы создать рефлексивные и транзитивные отношения.

{-# LANGUAGE ScopedTypeVariables, TypeOperators, MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, AllowAmbiguousTypes, OverlappingInstances #-}

import Control.Monad.Identity
import Data.Maybe

class x !<=! y where
  repr :: x a -> y a

instance x !<=! x where
  repr = id

instance Identity !<=! Maybe where
  repr = return . runIdentity

instance Maybe !<=! [] where
  repr = maybeToList

instance (x !<=! y, y !<=! z) => x !<=! z where
  repr = r2 . r1
    where r1 :: x a -> y a
          r1 = repr
          r2 :: y a -> z a
          r2 = repr

примечание: я пробовал это на GHC 7.8. Возможно, вам придется удалить AllowAmbiguousTypes.

Изменить: я хотел бы сделать что-то вроде repr (Identity 3 :: Identity Int) :: [Int]


typeclass haskell
person Boldizsár Németh    schedule 16.07.2014    source источник
comment
Разве вам не нужны несвязные экземпляры для этого?   -  person n. 1.8e9-where's-my-share m.    schedule 16.07.2014
comment
С непоследовательными экземплярами я получаю Context reduction stack overflow; size = 21   -  person Boldizsár Németh    schedule 16.07.2014
comment
Вывод типа не может работать так. Откуда компилятору известно, что A <= B, A <= A <= B или A <= A <= A <= ... <= B дают один и тот же результат? Вы можете легко определить экземпляр T <= T для некоторого T, чтобы T <= T <= T и T <= T фактически производили разные функции. Вы можете сделать что-то с функциями типов, в которых вы берете список отношений и пытаетесь создать целевое отношение. Или вы можете сделать так, чтобы функция repr принимала аргумент, определяющий путь. Но это не может произойти автоматически (волшебным образом).   -  person user2407038    schedule 16.07.2014
comment
Как я понял, вам нужно использовать расширение UndecidableInstances для instance x !<=! x where. Может еще нужны FlexibleInstances, OverlappingInstances, IncoherentInstances.   -  person viorior    schedule 16.07.2014
comment
viorior: в настоящее время используются гибкие и перекрывающиеся экземпляры, несогласованные экземпляры вызывают переполнение стека сокращения контекста.   -  person Boldizsár Németh    schedule 16.07.2014
comment
Вы можете сделать это без вывода, явно представив свои условия доказательства, например. ГАДТ. В этом случае вы должны указать морфизмы; в зависимости от вашей цели, это может быть приемлемо.   -  person luqui    schedule 17.07.2014

Ответы (2)


arrow_upward
6
arrow_downward

Проблема в том, что мы не можем заставить GHC выполнять общий поиск экземпляров по графу. В данном конкретном случае было бы даже неплохо, если бы GHC мог выполнять алгоритм кратчайшего пути, поскольку наша функция становится медленнее с каждым промежуточным представлением в пути.

Однако мы можем сделать поиск однозначным в каждом узле графа, ограничив количество исходящих ребер одним, и GHC справится с этим. Это означает, что каждый тип имеет не более одного прямого представления:

{-# LANGUAGE FlexibleInstances, TypeOperators, MultiParamTypeClasses, FunctionalDependencies, UndecidableInstances, OverlappingInstances #-}

import Control.Monad.Identity
import Data.Maybe

class DirectRepr x y | x -> y where
    directRepr :: x a -> y a

Мы можем построить график с DirectRepr:

instance DirectRepr Identity Maybe where
    directRepr (Identity a) = Just a

instance DirectRepr Maybe [] where
    directRepr = maybeToList

а затем пройти его с классом-оболочкой <=:

class x <= y where
    repr :: x a -> y a

instance x <= x where
    repr = id

instance (DirectRepr x y, y <= z) => x <= z where
    repr = repr . directRepr

main = print (repr (Identity ()) :: [()]) -- [()]

Он работает и с циклическими графами, поскольку поиск останавливается, когда мы сталкиваемся с случаем рефлексивности для <= (спасибо OverlappingInstances):

data A a
data B a
data C a

instance DirectRepr A B where directRepr = undefined 
instance DirectRepr B C where directRepr = undefined
instance DirectRepr C A where directRepr = undefined

foo :: A Int
foo = repr (undefined :: B Int)

Если начальный тип приводит к циклу, а в цикле нет типа конечной точки, поиск зависает, и мы получаем переполнение контекста. Это не должно нас сильно беспокоить, поскольку делает ошибку переполнения контекста эквивалентной простой ошибке «нет экземпляра».

bar :: Maybe Int -- context overflow
bar = repr (undefined :: A Int)
person András Kovács    schedule 16.07.2014
comment
Интересно, можно ли использовать пакет constraints для решения этой проблемы лучше. - person András Kovács; 16.07.2014
comment
Спасибо, Андраш. К сожалению, одно прямое представление для меня бесполезно. Простейшая структура представления, которую я хочу получить, это следующая DAG: Identity :<=: Maybe :<=: [] :<=: ListT IO, Identity :<=: IO :<=: MaybeT IO :<=: ListT IO, Maybe :<=: MaybeT IO - person Boldizsár Németh; 16.07.2014

arrow_upward
2
arrow_downward

Это может быть невозможно сделать только путем вывода. Я сделал еще одно решение, используя Template Haskell, генерируя все экземпляры, которые могут быть получены из более простых. Использование библиотеки выглядит следующим образом:

$(makeMonadRepr ''Identity          ''Maybe                     [e| return . runIdentity |])
$(makeMonadRepr ''Identity          ''IO                        [e| return . runIdentity |])
$(makeMonadRepr ''Maybe             [t| MaybeT IO |]            [e| MaybeT . return |])
$(makeMonadRepr ''IO                [t| MaybeT IO |]            [e| MaybeT . liftM Just |])
$(makeMonadRepr ''Maybe             TH.ListT                    [e| maybeToList |])
$(makeMonadRepr TH.ListT            [t| Trans.ListT IO |]       [e| Trans.ListT . return |])
$(makeMonadRepr ''IO                [t| Trans.ListT IO |]       [e| Trans.ListT . liftM (:[]) |])
$(makeMonadRepr [t| MaybeT IO |]    [t| Trans.ListT IO |]       [e| Trans.ListT . liftM maybeToList . runMaybeT |])

Это генерирует все экземпляры, которые могут быть получены из рефлексивности или транзитивности. После вставки нового узла с вызовом makeMonadRepr создаются все производные ребра, поэтому пользователь может расширить такую ​​структуру.

Возможно, это не самое элегантное решение, поэтому я открыт для других идей.

person Boldizsár Németh    schedule 16.07.2014
comment
Обратите внимание, что TH.ListT эквивалентно [], а Trans.ListT на самом деле ListT. - person Boldizsár Németh; 16.07.2014