Базовый вопрос о мономорфизме / полиморфизме Хаскелла (HList)

Question

Я новичок в Haskell и Stackru, и вот мой первый и, вероятно, довольно простой вопрос по 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)

Спасибо, _c

Answer 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 тип обоих аргументов для одной переменной типа, последний не делает: второй аргумент просто l ограничено тем, что должен быть какой-то случай RList для этого l). Поскольку нет подписи типа для rc (обратите внимание, что если вы предоставите один из ваших исходных примеров проверок типов) и r1 и r2 имеют полиморфный, а не эквивалентный тип, rкомпилятор пытается найти определение экземпляра для RList r (HCons (R r1 Double) HNil) (r исходит из 1-го аргумента и r1 - со 2-го) и не может этого сделать. С помощью ограничения эквивалентности типов мы определяем экземпляр RList с двумя различными r1 а также r2 с единственным условием, что они должны быть эквивалентны, поэтому похоже, что GHC связывает их с той же самой переменной полиморфного типа при разрешении экземпляра RList за l,