Я изучаю то, что Haskell может предложить на своем пути к зависимым типам, читая Thinking with types
.
Вот гетерогенный список, определенный как GADT.
data HList (ts :: [Type]) where
HNil :: HList '[]
(:#) :: t -> HList ts -> HList (t ': ts)
infixr 5 :#
instance Eq (HList '[]) where
HNil == HNil = True
instance (Eq t, Eq (HList ts)) => Eq (HList (t ': ts)) where
(a :# as) == (b :# bs) = a == b && as == bs
instance Ord (HList '[]) where
compare HNil HNil = EQ
instance (Ord t, Ord (HList ts)) => Ord (HList (t ': ts)) where
compare (a :# as) (b :# bs) = case compare a b of
EQ -> compare as bs
x -> x
instance Show (HList '[]) where
show HNil = "[]"
instance (Show t, Show (HList ts)) => Show (HList (t ': ts)) where
show xs = "[" ++ (show' xs "") ++ "]"
where
show' (y :# ys) prefix = prefix ++ (show y) ++ rest
where rest = case of
HNil -> ""
_ -> show' ys ", "
Вот ошибка, которую я получаю.
• Occurs check: cannot construct the infinite type: ts2 ~ t1 : ts2
Expected type: HList ts2 -> [Char] -> [Char]
Actual type: HList ts1 -> p -> p1
• In the expression: show' ys ", "
In a case alternative: _ -> show' ys ", "
In the expression:
case ys of
HNil -> ""
_ -> show' ys ", "
• Relevant bindings include
ys :: HList ts2 (bound at src/Lib.hs:43:25)
y :: t1 (bound at src/Lib.hs:43:20)
|
46 | _ -> show' ys ", "
Я читаю исходный код HList, и то, что они делают, это то, что я считаю уродливым взломом, когда они сопоставляют шаблон с строкой, возвращаемой из show ys
, и если она равна []
затем остановите рекурсию в принципе, что я считаю хаком.