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

Question

Потерпи меня, если это глупый вопрос. Как я могу набрать универсальную функцию, которая принимает две записи и возвращает массив их общих полей?

Допустим, у меня есть:

type A = { name :: String, color :: String }
type B = { name :: String, address :: Address, color :: String }

myImaginaryFunction :: ???
-- should return ["name", "color"] :: Array of [name color]

Я хочу написать функцию, которая принимает ЛЮБОЕ два типа записей и возвращает массив общих полей. Решение haskell также подойдет.

Answer 1

Для выражения двух типов записей с общими полями в 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"],

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

Answer 2

Что касается Haskell, мне нравится ответ К. А. Бура, но лично я бы не использовал Typeable и вместо этого использовал Generics GHC. Я думаю, что это может быть предпочтением на данный момент, хотя.

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

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

Union r1' r r1

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

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

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 With PureScript 2nd Edition.

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

Если все это кажется слишком сложным, ваше другое решение может заключаться в приведении записей в String Map и получении объединенного набора ключей. Я не знаю, является ли это ответом в Elm, так как представление String Map во время выполнения, вероятно, не соответствует Record. Но для PureScript это одна из опций, так как представление во время выполнения StrMap такое же, как запись.

Answer 3

На самом деле, подумав об этом, я думаю, можно сделать то, что вы действительно хотите сделать в современном 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 в виде символа синглтона SSymbol s Функция удобства with_ сделаем этот синглтон неявным:

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) используя шаблон 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 пакет и шаблон 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

Опять же, библиотека синглетонов здесь действительно замечательна. Я использую мой автоматически сгенерированный Common функция уровня типа вместе с одноэлементным уровнем sElem функция (которая автоматически генерируется в 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

Answer 4

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

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

Так:

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

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

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

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