Полиморфная функция внутри семейства типов

Я пытаюсь определить функцию внутри семейства типов, которая полиморфна фантомному типу самого GADT, определенного в семействе типов.

Мое определение семейства типов выглядит следующим образом:

class Channel t where
    data Elem t a :: * 
    foo :: t -> Elem t a
    bar :: Elem t a -> [a]

У меня есть такой пример:

data MyChannelType = Ch

instance Channel MyChannelType where

    data Elem MyChannelType a where
        MyConstructor :: Char -> Elem MyChannelType Char

    foo _ = MyConstructor 'a'

    bar (MyConstructor c) = repeat c

Компилятор жалуется, что:

Couldn't match type ‘a’ with ‘Char’
      ‘a’ is a rigid type variable bound by
          the type signature for foo :: MyChannelType -> Elem MyChannelType a

Можно ли написать эту функцию с помощью Rank2Types или переформулировать мои типы данных, чтобы включить ее?

РЕДАКТИРОВАТЬ: в ответ на разъяснения Ганеш запросил

Я бы хотел, чтобы foo (bar Ch) :: [Int] был незаконным.

Я использовал в точности решение, которое предлагает Ганеш, но меня мотивирует следующий более сложный пример, где он падает; данный:

data MyOtherType = IntCh | StringCh

У меня есть такой пример:

instance Channel MyOtherType where

    data Elem MyOtherType a where
        ElemInt    :: Int ->    Elem MyOtherType Int
        ElemString :: String -> Elem MyOtherType String

    foo IntCh    = ElemInt 0
    foo StringCh = ElemString "a"

    bar (ElemInt i)    = repeat i
    bar (ElemString s) = repeat s

Большое спасибо,

Майкл


typeclass haskell type-level-computation type-families
person Michael Thomas    schedule 12.08.2014    source источник
comment
Это невозможно с вашими текущими подписями. Что бы вы ожидали от bar (foo Ch) :: [Int], чтобы помочь понять варианты его переформулирования?   -  person GS - Apologise to Monica    schedule 12.08.2014
comment
или, в качестве альтернативы, вы бы хотели сделать это незаконным?   -  person GS - Apologise to Monica    schedule 12.08.2014

Ответы (2)


arrow_upward
5
arrow_downward

С указанными вами подписями foo нереализуем для MyChannelType, потому что он утверждает, что может создавать Elem MyChannelType a для любого a типа.

Если вы действительно хотите, чтобы для данного t был только один a тип, вы можете использовать функцию типа, чтобы выразить это:

class Channel t where
    data Elem t a :: *
    type Contents t :: *

    foo :: t -> Elem t (Contents t)
    bar :: Elem t a -> [a]

а затем добавить

type Contents MyChannelType = Char

к экземпляру.

В ответ на ваше изменение я бы разделил Channel на два класса:

class Channel t where
    data Elem t a :: *
    bar :: Elem t a -> [a]

class Channel t => ChannelContents t a where
    foo :: t -> Elem t a

Затем вы можете определить MyOtherType экземпляры с помощью:

instance Channel MyOtherType where

    data Elem MyOtherType a where
        ElemInt :: Int -> Elem MyOtherType Int
        ElemString :: String -> Elem MyOtherType String

    bar (ElemInt i) = repeat i
    bar (ElemString s) = repeat s

instance ChannelContents MyOtherType Int where
    foo IntCh = ElemInt 0

instance ChannelContents MyOtherType String where
    foo StringCh = ElemString "a"

Вам нужно будет включить несколько расширений: MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances (последние два только из-за экземпляра String).

person GS - Apologise to Monica    schedule 12.08.2014
comment
Привет, Ганеш. Спасибо за это - я немного горжусь тем, что именно этим я и занимался до сих пор! Однако у меня есть более сложный случай, когда это не удается - я добавил детали к исходному вопросу. Я понимаю, что это, вероятно, требует переосмысления, любой был бы признателен за любые предложения по изменению формулировки. С уважением, Майкл - person Michael Thomas; 12.08.2014

arrow_upward
2
arrow_downward

В качестве более общей альтернативы решению Ганеша вы также можете ограничить переменную a целым классом типов (возможно, только одним):

{-# LANGUAGE ConstraintKinds #-}
import GHC.Exts (Constraint)

class Channel t where
    data Elem t a :: *
    type ElemConstraint t a :: Constraint
    foo :: ElemConstraint t a => t -> Elem t a
    bar :: ElemConstraint t a => Elem t a -> [a]

instance Channel MyChannelType where
    data Elem MyChannelType a where
        MyConstructor :: Char -> Elem MyChannelType Char
    type ElemConstraint t a = a ~ Char
    foo _ = MyConstructor 'a'
    bar (MyConstructor c) = repeat c


class OtherType_Class c where
  mkOtherTypeElem :: c -> Elem MyOtherType c
  evOtherTypeElem :: Elem MyOtherType c -> c

instance OtherType_Class Int where
  mkOtherTypeElem = ElemInt
  evOtherTypeElem (ElemInt i) = i
instance OtherType_Class String where
  ...

instance Channel MyOtherType where
    data Elem MyOtherType a where
        ElemInt    :: Int ->    Elem MyOtherType Int
        ElemString :: String -> Elem MyOtherType String
    type ElemConstraint MyOtherType a = OtherType_Class a

Тем не менее, я должен сказать, что это довольно неудобная вещь для какого-то фиксированного набора типов.

person leftaroundabout    schedule 12.08.2014
comment
Интересно - я даже не понимал, что это можно выразить. Является ли это эквивалентом второго решения, предлагаемого Ганешем? - person Michael Thomas; 12.08.2014
comment
В основном эквивалентно, но в реальном коде он будет выглядеть немного иначе. Мне очень нравится ConstraintKinds, они работают лучше для ограничения одного типа, как в MyChannelType, и могут (но не обязательно) давать несколько более приятные подписи, чем с MultiParamTypeClasses. Для таких случаев, как MyOtherType, решение Ганеша лучше, потому что оно не требует такого неудобного выброса OtherType_Class. - person leftaroundabout; 12.08.2014