Можно ли использовать систему типов Haskell (GADT) для создания каких-то полиморфных вариантов? - PullRequest
Новая
       20

Можно ли использовать систему типов Haskell (GADT) для создания каких-то полиморфных вариантов?

0 голосов
/ 10 октября 2018

Вот что я пытаюсь достичь: 

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}

module Action where

import Data.Type.Set

data Configuration
  = A
  | B
  | C

data Action (configuration :: Configuration) where
  Action1 :: Member cfg '[ 'A ]     => Action cfg
  Action2 :: Member cfg '[ 'B, 'C ] => Action cfg
  Action3 :: Member cfg '[ 'A, 'C ] => Action cfg

exhaustive :: Action 'A -> ()
exhaustive Action1 = ()
exhaustive Action3 = ()

У меня есть набор действий и набор конфигураций, но некоторые действия имеют смысл только в некоторых конфигурациях.Мне бы не хотелось явно отбрасывать ненужные действия в конфигурации, поэтому я подумал об использовании GADT.К сожалению, средство проверки типов не может понять, что моя exhaustive функция действительно исчерпывающая.

Интересно, могу ли я использовать какой-либо из существующих списков / наборов на уровне типов или даже типы строк (как в http://hackage.haskell.org/package/row-types-0.2.3.0/docs/Data-Row-Variants.html), чтобы решить эту проблему.

Я также попробовал подход, где Action2 :: Action '[ 'B, 'C ] и выдвижение ограничений класса типов в exhaustive, но безуспешно.

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

1 Ответ

0 голосов
/ 10 октября 2018

Друг предложил решение: 

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

module Action where

type family MemberB (x :: k) (l :: [k]) where
  MemberB x '[]     = 'False
  MemberB x (x:xs)  = 'True
  MemberB x (x':xs) = MemberB x xs

type Member x xs = MemberB x xs ~ 'True

data Configuration
  = A
  | B
  | C

data Action (configuration :: Configuration) where
  Action1 :: Member cfg '[ 'A ]     => Action cfg
  Action2 :: Member cfg '[ 'B, 'C ] => Action cfg
  Action3 :: Member cfg '[ 'A, 'C ] => Action cfg

exhaustive :: Action 'A -> ()
exhaustive Action1 = ()
exhaustive Action3 = ()
exhaustive Action2 = ()

Очевидно, проблема в том, что Member, который я использовал (из Data.Type.Set), не принадлежал к семейству закрытых типов.Теперь сообщения об ошибках невелики, и мы попытались сделать следующее: 

type family MemberB (x :: k) (l :: [k]) where
  MemberB x '[]     = TypeError ('Text "not a member")
  MemberB x (x:xs)  = 'True
  MemberB x (x':xs) = MemberB x xs

Но, к сожалению, это приводит к ошибке типа!Это потому, что TypeError счастливо объединится с 'True?Если у кого-то есть решение, чтобы сделать ошибку типа немного приятнее, я с радостью приму ее!

Я сделал для этого отдельный вопрос:

Как определить ошибку нестандартного типавнутри семейства типов для ограничения, использующего равенство типов?

...