Основной вопрос о мономорфизме/полиморфизме Haskell (HList)

Я новичок в Haskell и Stackoverflow, и вот мой первый и, вероятно, довольно простой вопрос о Haskell.

module M where

import Data.HList

data R r a 

r1 = undefined :: R a Int
r2 = undefined :: R a Double

rPair :: R r a -> R r b -> (R r a, R r b)
rPair = (,)

rp = rPair r1 r2

Это имеет смысл, даже если r1 и r2 полиморфны в r, rPair выравнивает их тип r в соответствии с сигнатурой типа. Есть ли технический термин для этого «выравнивания»?

class HList l => RList r l
instance RList r HNil
instance RList r l => RList r (HCons (R r a) l)

rCons :: RList r l => R r a -> l -> (HCons (R r a) l)
rCons = hCons

rc = rCons r1 (rCons r2 hNil)

rCons отлично работает, если переданные R мономорфны в r, ограничивая тип r списка по желанию. но если они полиморфны в r, он не выравнивает их так, как это делает rPair, и выдает ошибку (определение rc выше).

No instance for (RList r (HCons (R r1 Double) HNil))

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

r1 = undefined :: R a Int
r2 = undefined :: R a Double

rc :: HCons (R a Int) (HCons (R a Double) HNil)
rc = rCons r1 (rCons r2 hNil)

Спасибо, _с


person polypus74    schedule 04.03.2011    source источник
comment
обновление: если я изменю его на 'class HList l => RList r l | l -> r', с UndecidableInstances и FunctionalDependencies компилируется с rc::HCons(R GHC.Prim.Any Int)(HCons(R GHC.Prim.Any Double)HNil). теперь просто нужно выяснить, что это на самом деле означает   -  person polypus74    schedule 05.03.2011
comment
С функциональными зависимостями | l -> r часто можно прочитать как l однозначно определяет r. Помогает ли это вашей интуиции? Кроме того, то, что вы назвали выравниванием/выравниванием, я бы назвал унифицированным. Система типов Haskell основана на унификации (точно так же, как оценка Пролога).   -  person stephen tetley    schedule 05.03.2011
comment
Просто чтобы заверить всех, кто читает это, это не нубский вопрос Haskell. Я считаю, что выравнивание известно как унификация, и говорят, что типы унифицированы. Но это основано на том, что говорит средство проверки типов, когда ему не удается сопоставить типы, поэтому я могу ошибаться.   -  person Paul Johnson    schedule 05.03.2011


Ответы (1)


Чтобы ответить на ваш второй вопрос, вы можете использовать ограничение эквивалентности типов (из расширения TypeFamilies), чтобы ослабить определение экземпляра RList:

class HList l => RList r l
instance RList r HNil
instance (RList r1 l, r1 ~ r2) => RList r1 (HCons (R r2 a) l)

Теперь ваш rc будет приведен к нужному типу.

Я не думаю, что смогу «ясно объяснить» это явление (кто-нибудь обязательно это сделает), но очевидно, что разница между rPair и rCons заключается в том, что в то время как первый связывает r тип обоих аргументов с переменной одного и того же типа, последний не 't: второй аргумент просто l ограничен тем, что должен быть какой-то экземпляр RList для этого l). Поскольку для rc нет сигнатуры типа (обратите внимание, что если вы предоставите ее в исходном примере проверки типов), а r1 и r2 имеют полиморфные, не эквивалентные, r, компилятор пытается найти определение экземпляра для RList r (HCons (R r1 Double) HNil) ( r происходит от 1-го аргумента, а r1 - от 2-го) и не может этого сделать. С ограничением эквивалентности типов мы определяем экземпляр RList с двумя разными r1 и r2 с единственным условием, что они должны быть эквивалентны, поэтому похоже, что GHC связывает их с одной и той же переменной полиморфного типа при разрешении экземпляра RList для l.

person Ed'ka    schedule 05.03.2011