вывести тип для общих полей в двух записях

Чтобы выразить два типа записей с общими полями в Haskell, вам понадобится расширение GHC:

{-# LANGUAGE DuplicateRecordFields #-}

и для самоанализа имен полей вам понадобятся дженерики на основе класса Data:

{-# LANGUAGE DeriveDataTypeable #-}
import Data.Data ( Data, Typeable, DataRep(AlgRep), dataTypeRep
                 , dataTypeOf, constrFields)
import Data.List (intersect)
import Data.Proxy (Proxy(..), asProxyTypeOf)

Это позволит вам определить два типа данных, используя одинаковые имена полей:

data Address = Address String deriving (Typeable, Data)
data A = A { name :: String, color :: String }
    deriving (Typeable, Data)
data B = B { name :: String, address :: Address, color :: String}
    deriving (Typeable, Data)

а затем вы можете получить имена полей, используя:

fieldNames :: (Data t) => Proxy t -> [String]
fieldNames t = case dataTypeRep $ dataTypeOf $ asProxyTypeOf undefined t of
  AlgRep [con] -> constrFields con

и получить общие поля с:

commonFields :: (Data t1, Data t2) => Proxy t1 -> Proxy t2 -> [String]
commonFields t1 t2 = intersect (fieldNames t1) (fieldNames t2)

После чего будет работать следующее:

ghci> commonFields (Proxy :: Proxy A) (Proxy :: Proxy B)
["name", "color"]
ghci>

Обратите внимание, что реализация fieldNames выше предполагает, что будут проверяться только типы записей с одним конструктором. См. документацию для Data.Data, если вы хотите обобщить ее.

Теперь, поскольку вы вампир-помощник, я знаю, что вы потребуете функцию уровня типа, хотя в своем вопросе вы ничего не сказали о необходимости функции уровня типа! На самом деле, я вижу, вы уже добавили комментарий о том, как вы заинтересованы в том, чтобы каким-то образом вернуть массив name | color, хотя в Haskell такой вещи не существует, и хотя вы прямо сказали в своем вопросе, что ожидаете ответа на уровне термина ["name", "color"].

Тем не менее, могут быть не вампиры с подобным вопросом, и, возможно, этот ответ поможет им вместо этого.

Для Haskell мне нравится K.A. Ответ Бура, но лично я бы не стал использовать Typeable и вместо этого использовал GHC Generics. Я думаю, что это может быть предпочтением на данный момент.

Для PureScript я писал об этой проблеме в своем блоге Создание различий для записей разных типов в PureScript ранее в этом месяце. Подход полностью отличается от того, что у вас есть с языками, у которых нет типов строк (нет, у Elm их нет. Вы действительно не получите там решения, кроме использования однородной карты строк).

Прежде всего, если вы знакомы с PureScript, вы можете использовать Union, но это тоже не сработает, так как вы хотите сделать что-то вроде:

Union r1' r r1

Где r1' будет дополнением общего подтипа r между вашей первой записью r1 и r2. Причина в том, что здесь у вас есть две нерешенные переменные, а функциональные зависимости Union требуют решения для любых двух из трех параметров Union.

Итак, поскольку мы не можем использовать Union напрямую, нам придется придумать какое-то решение. Поскольку я могу получить структуру RowList, отсортированную по ключам, я решил использовать ее, чтобы пройтись по RowList двух разных записей и выйти из пересечения:

class RowListIntersection
  (xs :: RowList)
  (ys :: RowList)
  (res :: RowList)
  | xs ys -> res

instance rliNilXS :: RowListIntersection Nil (Cons name ty tail) Nil
instance rliNilYS :: RowListIntersection (Cons name ty tail) Nil Nil
instance rliNilNil :: RowListIntersection Nil Nil Nil
instance rliConsCons ::
  ( CompareSymbol xname yname ord
  , Equals ord EQ isEq
  , Equals ord LT isLt
  , Or isEq isLt isEqOrLt
  , If isEq xty trashty yty
  , If isEq xty trashty2 zty
  , If isEq (SProxy xname) trashname (SProxy zname)
  , If isEq
      (RLProxy (Cons zname zty res'))
      (RLProxy res')
      (RLProxy res)
  , If isEqOrLt
      (RLProxy xs)
      (RLProxy (Cons xname xty xs))
      (RLProxy xs')
  , If isLt
      (RLProxy (Cons xname yty ys))
      (RLProxy ys)
      (RLProxy ys')
  , RowListIntersection xs' ys' res'
  ) => RowListIntersection (Cons xname xty xs) (Cons yname yty ys) res

Затем я использовал короткое определение для получения ключей полученного RowList:

class Keys (xs :: RowList) where
  keysImpl :: RLProxy xs -> List String

instance nilKeys :: Keys Nil where
  keysImpl _ = mempty

instance consKeys ::
  ( IsSymbol name
  , Keys tail
  ) => Keys (Cons name ty tail) where
  keysImpl _ = first : rest
    where
      first = reflectSymbol (SProxy :: SProxy name)
      rest = keysImpl (RLProxy :: RLProxy tail)

Итак, вместе я могу определить такую ​​функцию, чтобы получить общие метки:

getSharedLabels
  :: forall r1 rl1 r2 rl2 rl
  . RowToList r1 rl1
  => RowToList r2 rl2
  => RowListIntersection rl1 rl2 rl
  => Keys rl
  => Record r1
  -> Record r2
  -> List String
getSharedLabels _ _ = keysImpl (RLProxy :: RLProxy rl)

Затем мы можем увидеть ожидаемые результаты:

main = do
  logShow <<< Array.fromFoldable $
    getSharedLabels
      { a: 123, b: "abc" }
      { a: 123, b: "abc", c: true }
  -- logs out ["a","b"] as expected

Если вы новичок в RowList/RowToList, вы можете прочитать мой Слайды RowList Fun с PureScript 2nd Edition.

Я разместил код для этого ответа здесь.

На самом деле, подумав еще немного, я думаю, что можно делать то, что вы на самом деле хотите сделать в современном Haskell, если то, что вы на самом деле > нужно работать с типом записи с именованными полями на уровне типа, в том числе делать такие вещи, как получение нового типа записи во время компиляции с использованием общих полей из двух других записей.

Это немного сложно и немного уродливо, хотя некоторые части работают на удивление хорошо. Да, конечно, это «слишком много церемоний для такой простой задачи», но имейте в виду, что мы пытаемся реализовать совершенно новую, нетривиальную функцию уровня типа (своего рода зависимая структурная типизация). Единственный способ упростить эту задачу — встроить функцию в язык и его систему типов с самого начала; иначе будет сложно.

В любом случае, пока мы не получим расширение DependentTypes, вы должны явно включить небольшое количество (ха-ха) расширений:

{-# LANGUAGE AllowAmbiguousTypes       #-}
{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE KindSignatures            #-}
{-# LANGUAGE ScopedTypeVariables       #-}
{-# LANGUAGE TemplateHaskell           #-}
{-# LANGUAGE TypeApplications          #-}
{-# LANGUAGE TypeFamilies              #-}
{-# LANGUAGE TypeInType                #-}
{-# LANGUAGE TypeOperators             #-}
{-# LANGUAGE UndecidableInstances      #-}
{-# OPTIONS_GHC -Wincomplete-patterns  #-}

module Records where

Мы будем довольно часто использовать пакет singletons и его подмодули: Prelude для основных функций уровня типа, таких как Map, Fst и Lookup; модуль TH для создания собственных одноэлементных и продвинутых функций с помощью сплайсов Template Haskell; и TypeLits для работы с типом Symbol (т. е. строковыми литералами на уровне типа).

import Data.Singletons.Prelude
import Data.Singletons.TH
import Data.Singletons.TypeLits

Нам также понадобятся некоторые другие шансы и концы. Text нужен только потому, что это неподнятая ("пониженная") версия Symbol.

import Data.Function ((&))
import Data.Kind (Type)
import Data.List (intersect)
import qualified Data.Text as Text

Мы не сможем работать с обычными записями Haskell. Вместо этого мы определим конструктор типа Record. Этот конструктор типов будет проиндексирован списком пар (Symbol, Type), где Symbol задает имя поля, а Type задает тип значения, хранящегося в этом поле.

data Record :: [(Symbol, Type)] -> Type where

Уже сейчас есть несколько важных последствий для этого дизайнерского решения:

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

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

В любом случае, вернемся к нашему конструктору типа Record. Будет два конструктора данных, конструктор Record для создания пустой записи:

  Record :: Record '[]

и конструктор With для добавления поля в запись:

  With :: SSymbol s -> t -> Record fs -> Record ('(s, t) : fs)

Обратите внимание, что With требует представителя времени выполнения для s :: Symbol в виде символа singleton SSymbol s Вспомогательная функция with_ сделает этот singleton неявным:

with_ :: forall s t fs . (SingI s) => t -> Record fs -> Record ('(s, t) : fs)
with_ = With sing

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

rec1 :: Record '[ '("bar", [Char]), '("foo", Int)]
rec1 = Record & with_ @"foo" (10 :: Int)
              & with_ @"bar" "Hello, world"
-- i.e., rec1 = { foo = 10, bar = "Hello, world" } :: { foo :: Int, bar :: String }

rec2 :: Record '[ '("quux", Maybe Double), '("foo", Int)]
rec2 = Record & with_ @"foo" (20 :: Int)
              & with_ @"quux" (Just 1.0 :: Maybe Double)
-- i.e., rec2 = { foo = 20, quux = Just 1.0 } :: { foo :: Int, quux :: Maybe Double }

Чтобы доказать, что этот тип записи полезен, мы определим типобезопасный метод доступа к полю. Вот тот, который использует явный синглтон для выбора поля:

field :: forall s t fs . (Lookup s fs ~ Just t) => SSymbol s -> Record fs -> t
field s (With s' t r)
  = case s %:== s' of
      STrue -> t
      SFalse -> field s r

и помощник с неявным синглтоном:

field_ :: forall s t fs . (Lookup s fs ~ Just t, SingI s) => Record fs -> t
field_ = field @s sing

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

exField = field_ @"foo" rec1

Обратите внимание, что попытка доступа к несуществующему полю не приведет к проверке типов. Сообщение об ошибке не идеально, но, по крайней мере, это ошибка времени компиляции:

-- badField = field_ @"baz" rec1  -- gives: Couldn't match type Nothing with Just t

Определение field намекает на мощь библиотеки singletons. Мы используем функцию уровня типа Lookup, которая была автоматически сгенерирована с помощью Template Haskell из определения уровня термина, которое выглядит точно так же, как показано ниже (взято из источника singletons и переименовано во избежание конфликтов):

lookup'                  :: (Eq a) => a -> [(a,b)] -> Maybe b
lookup' _key []          =  Nothing
lookup'  key ((x,y):xys) = if key == x then Just y else lookup' key xys

Используя только контекст Lookup s fs ~ Just t, GHC может определить, что:

1. Поскольку контекст подразумевает, что это поле будет найдено в списке, второй аргумент field никогда не может быть пустой записью Record, поэтому нет предупреждения о неполных шаблонах для field, и фактически вы получите ошибку типа, если попытаетесь чтобы обработать это как ошибку времени выполнения, добавив случай: field s Record = error "ack, something went wrong!"

2. Рекурсивный вызов field корректен по типу, если мы находимся в ветке SFalse. То есть GHC выяснил, что если мы можем успешно Lookup найти ключ s в списке, но он не находится в начале, мы должны иметь возможность найти его в конце.

(Это удивительно для меня, но тем не менее...)

Это основы нашего типа записи. Для интроспекции имен полей либо во время выполнения, либо во время компиляции мы представим вспомогательную функцию, которую поднимем на уровень типа (т. е. функцию уровня типа Names) с помощью Template Haskell:

$(singletons [d|
  names :: [(Symbol, Type)] -> [Symbol]
  names = map fst
  |])

Обратите внимание, что функция уровня типа Names может предоставлять доступ во время компиляции к именам полей записи, например, в сигнатуре гипотетического типа:

data SomeUIType fs = SomeUIType -- a UI for the given compile-time list of fields
recordUI :: Record fs -> SomeUIType (Names fs)
recordUI _ = SomeUIType

Однако более вероятно, что мы захотим работать с именами полей во время выполнения. Используя Names, мы можем определить следующую функцию, которая берет запись и возвращает список имен полей в виде синглтона. Здесь SNil и SCons — одноэлементные эквиваленты терминов [] и (:).

sFields :: Record fs -> Sing (Names fs)
sFields Record = SNil
sFields (With s _ r) = SCons s (sFields r)

А вот версия, которая возвращает [Text] вместо синглтона.

fields :: Record fs -> [Text.Text]
fields = fromSing . sFields

Теперь, если вы просто хотите получить список общих полей двух записей во время выполнения, вы можете сделать:

rec12common = intersect (fields rec1) (fields rec2)
-- value:  ["foo"]

Как насчет создания типа с общими полями во время компиляции? Ну, мы можем определить следующую функцию, чтобы получить набор полей с левым смещением с общими именами. (Это «смещение влево» в том смысле, что если совпадающие поля в двух записях имеют разные типы, он примет тип первой записи.) Опять же, мы используем пакет singletons и Template Haskell, чтобы поднять его до типа- уровень Common функция:

$(singletons [d|
  common :: [(Symbol,Type)] -> [(Symbol,Type)] -> [(Symbol,Type)]
  common [] _ = []
  common (x@(a,b):xs) ys
    = if elem a (map fst ys)
      then x:common xs ys
      else   common xs ys
  |])

Это позволяет нам определить функцию, которая принимает две записи и сводит первую запись к набору полей с теми же именами, что и поля во второй записи:

reduce :: Record fs1 -> Record fs2 -> Record (Common fs1 fs2)
reduce Record _ = Record
reduce (With s x r1) r2
  = case sElem s (sFields r2) of STrue  -> With s x (reduce r1 r2)
                                 SFalse -> reduce r1 r2

Опять же, библиотека singletons здесь действительно замечательна. Я использую свою автоматически сгенерированную функцию уровня типа Common вместе с функцией sElem уровня singleton (которая автоматически создается в пакете singletons из определения уровня термина функции elem). Каким-то образом, несмотря на всю эту сложность, GHC может понять, что если sElem оценивается как STrue, я должен включить s в список общих полей, а если он оценивается как SFalse, я не должен. Попробуйте поиграться с результатами кейса справа от стрелок — вы не сможете заставить их проверить тип, если ошибетесь!

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

rec3 :: Record '[ '("foo", Int)]
rec3 = reduce rec1 rec2

Как и для любой другой записи, у меня есть доступ к именам полей во время выполнения и проверка типов доступа к полям во время компиляции:

-- fields rec3           gives  ["foo"], the common field names
-- field_ @"foo" rec3    gives  10, the field value for rec1

Обратите внимание, что, как правило, reduce r1 r2 и reduce r2 r1 будут возвращать не только разные значения, но и разные типы, если порядок и/или типы полей общих имен различаются между r1 и r2. Изменение этого поведения, вероятно, потребует пересмотра тех ранних и далеко идущих дизайнерских решений, о которых я упоминал ранее.

Для удобства вот вся программа, протестированная с использованием Stack lts-10.5 (с синглтонами 2.3.1):

{-# LANGUAGE AllowAmbiguousTypes       #-}
{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE KindSignatures            #-}
{-# LANGUAGE ScopedTypeVariables       #-}
{-# LANGUAGE TemplateHaskell           #-}
{-# LANGUAGE TypeApplications          #-}
{-# LANGUAGE TypeFamilies              #-}
{-# LANGUAGE TypeInType                #-}
{-# LANGUAGE TypeOperators             #-}
{-# LANGUAGE UndecidableInstances      #-}
{-# OPTIONS_GHC -Wincomplete-patterns  #-}

module Records where

import Data.Singletons.Prelude
import Data.Singletons.TH
import Data.Singletons.TypeLits
import Data.Function ((&))
import Data.Kind (Type)
import Data.List (intersect)
import qualified Data.Text as Text

data Record :: [(Symbol, Type)] -> Type where
  Record :: Record '[]
  With :: SSymbol s -> t -> Record fs -> Record ('(s, t) : fs)

with_ :: forall s t fs . (SingI s) => t -> Record fs -> Record ('(s, t) : fs)
with_ = With sing

rec1 :: Record '[ '("bar", [Char]), '("foo", Int)]
rec1 = Record & with_ @"foo" (10 :: Int)
              & with_ @"bar" "Hello, world"
-- i.e., rec1 = { foo = 10, bar = "Hello, world" } :: { foo :: Int, bar :: String }

rec2 :: Record '[ '("quux", Maybe Double), '("foo", Int)]
rec2 = Record & with_ @"foo" (20 :: Int)
              & with_ @"quux" (Just 1.0 :: Maybe Double)
-- i.e., rec2 = { foo = 20, quux = Just 1.0 } :: { foo :: Int, quux :: Maybe Double }

field :: forall s t fs . (Lookup s fs ~ Just t) => SSymbol s -> Record fs -> t
field s (With s' t r)
  = case s %:== s' of
      STrue -> t
      SFalse -> field s r

field_ :: forall s t fs . (Lookup s fs ~ Just t, SingI s) => Record fs -> t
field_ = field @s sing

exField = field_ @"foo" rec1
-- badField = field_ @"baz" rec1  -- gives: Couldn't match type Nothing with Just t

lookup'                  :: (Eq a) => a -> [(a,b)] -> Maybe b
lookup' _key []          =  Nothing
lookup'  key ((x,y):xys) = if key == x then Just y else lookup' key xys

$(singletons [d|
  names :: [(Symbol, Type)] -> [Symbol]
  names = map fst
  |])

data SomeUIType fs = SomeUIType -- a UI for the given compile-time list of fields
recordUI :: Record fs -> SomeUIType (Names fs)
recordUI _ = SomeUIType

sFields :: Record fs -> Sing (Names fs)
sFields Record = SNil
sFields (With s _ r) = SCons s (sFields r)

fields :: Record fs -> [Text.Text]
fields = fromSing . sFields

rec12common = intersect (fields rec1) (fields rec2)
-- value:  ["foo"]

$(singletons [d|
  common :: [(Symbol,Type)] -> [(Symbol,Type)] -> [(Symbol,Type)]
  common [] _ = []
  common (x@(a,b):xs) ys
    = if elem a (map fst ys)
      then x:common xs ys
      else   common xs ys
  |])

reduce :: Record fs1 -> Record fs2 -> Record (Common fs1 fs2)
reduce Record _ = Record
reduce (With s x r1) r2
  = case sElem s (sFields r2) of STrue  -> With s x (reduce r1 r2)
                                 SFalse -> reduce r1 r2

rec3 :: Record '[ '("foo", Int)]
rec3 = reduce rec1 rec2
-- fields rec3           gives  ["foo"], the common field names
-- field_ @"foo" rec3    gives  10, the field value for rec1

Что ж, поскольку ваша функция действительно возвращает массив строк, то тип возвращаемого значения должен быть просто Array String.

Типы аргументов будут генетическими, поскольку вы не знаете типы заранее. Если вы действительно хотите убедиться, что эти типы действительно являются записями, вы можете сделать свои общие параметры не самими записями, а типами строк, а затем ввести параметры-значения как Record a.

So:

myImaginaryFunction :: forall a b. Record a -> Record b -> Array String

Вот как вы вводите такую ​​функцию.

Или ваш вопрос действительно был о том, как это реализовать?

Также: вы заметили, что читерство (путем добавления тега Haskell) на самом деле не принесло вам никакой помощи, а только порицание? Пожалуйста, не делайте этого. Уважайте сообщество.