Типы ограничений в конструкторе GADT

У меня простой ADT

data Concept a = Entity  a |  Role a | Relation a | Resource a | Sub (Concept a)

Теперь я хочу создать GADT, используя этот ADT, который будет ограничивать сигнатуру типа его конструкторов. Этот код не будет работать, но я хочу сделать что-то вроде этого:

data Construct a b where
      Has :: Concept a -> 'Resource b -> Construct (Concept a) ('Resource b)

Т.е. Has конструктор для Construct может иметь параметр первого типа как Concept любой формы, но параметр второго типа должен быть конструктором Resource (повышенным до типа). Эта подпись не работает, поскольку я использую вид вместо типа. Но я хочу осознать нечто подобное и не могу понять, как сделать то же самое.

Я импортирую {-# LANGUAGE GADTs, TypeInType #-}.

Редактировать:

Основываясь на одном комментарии, если я сделаю это

 data Construct (a :: Concept ak) (b :: Concept bk)  where
  Has :: Construct a ('Resource b)

Тогда это проверка типов. Но теперь как мне извлечь значения при сопоставлении с образцом на Has

f :: Construct a b -> T.Text
f Has = ???

Мое требование: я хочу ограничить типы для конструктора Has a b, чтобы он мог разрешать только a :: Concept ak (т.е. любую концепцию) и (b ~ 'Resource *) => (b :: Concept bk) [1] (т.е. только тип ресурса концепции), например.

-- Concept values
person = Entity "person"
name = Resource "name"
role = Role "father"

-- I want this to be valid
personHasName = Has person name

-- And this to be invalid
personHasRole = Has person role

[1] - После некоторого чтения ограничений в видах, семействах типов и синглтон-типах я думаю, что можно реализовать такого рода ограничения с помощью этих принципов. Но я совершенно не в силах заставить его работать


type-constraints haskell dependent-type type-families gadt
person kaychaks    schedule 24.05.2017    source источник
comment
Забудьте о проблеме типа / типа, почему второй аргумент вашего конструктора является типом?   -  person Alec    schedule 24.05.2017
comment
Код здесь настолько тщательно продуман, а также так тщательно сокращен, что практически невозможно сказать, чего вы пытаетесь достичь. Не могли бы вы дать дополнительный контекст, объясняющий, что вы пытаетесь сделать, что вы хотите, чтобы эти типы значили, как вы собираетесь их использовать и т. Д.?   -  person dfeuer    schedule 24.05.2017
comment
Если вы хотите, чтобы ваш код проверял тип, просто удалите первый 'Resource: Has :: Concept a -> Construct (Concept a) ('Resource b). Но я предполагаю, что вы хотите, чтобы оба ваших полей были повышены до типов; в этом случае вам нужно что-то вроде Has :: Construct (x :: Concept a) ('Resource b); в этом случае вы, вероятно, также захотите объявить kind вашего типа: data Construct (a :: Concept ak) (b :: Concept bk) where Has :: Construct a ('Resource b)   -  person user2407038    schedule 24.05.2017
comment
@ user2407038: Я обновил сообщение на основе ваших предложений, но у меня есть еще несколько вопросов, которые я также добавил в сообщение.   -  person kaychaks    schedule 25.05.2017
comment
@dfeuer извиняюсь за неясность ранее, я отредактировал сообщение, добавив больше информации, и попытался уточнить свои намерения. Надеюсь, это поможет сейчас   -  person kaychaks    schedule 25.05.2017
comment
Я почти уверен, что вам нужна типовая семья Has :: Concept -> Constraint. Поскольку отношение Has не имеет семантики, вам нужно создавать смысл самостоятельно.   -  person Lazersmoke    schedule 25.05.2017

Ответы (1)


arrow_upward
3
arrow_downward

Спасибо Кейлу из # haskel-beginners за то, что он предложил это решение, представив фантомный тип и пометив его в Concept GADT

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

data ConceptType = EntityT | RoleT | RelationT | ResourceT | SubT ConceptType

data Concept (t :: ConceptType) a where
  Entity :: a -> Concept EntityT a
  Role :: a -> Concept RoleT a
  Relation :: a -> Concept RelationT a
  Resource :: a -> Concept ResourceT a
  Sub :: Concept t a -> Concept (SubT t) a

data Construct t a b where
  Has :: Concept t a -> Concept ResourceT b -> Construct t a b
person kaychaks    schedule 26.05.2017