mna*_*mna 2 haskell heterogeneous dependent-type
我在定义下面定义的异构列表的Show实例时遇到问题:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE FlexibleInstances #-}
import Data.Kind
data HList xs where
HNil :: HList TNil
(::^) :: a -> HList as -> HList (a :^ as)
data TypeList = TNil | (:^) Type TypeList
instance Show (HList TNil) where
show HNil = "[]"
Run Code Online (Sandbox Code Playgroud)
如果Typelist xs中的所有类型都有Show Instance,我想给HList xs一个show实例.我想一个人应该能写出类似的东西
instance (Show a, _) => Show (HList a :^ as) where
show (x ::^ xs) = show x ++ show xs
Run Code Online (Sandbox Code Playgroud)
但我不确定要填什么洞_.
PS:如果您在ghci中尝试此操作,请不要忘记添加语言扩展名
:set -XTypeInType -XTypeOperators
Run Code Online (Sandbox Code Playgroud)
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
import Data.Kind
infixr 5 ::^
data HList xs where
HNil :: HList TNil
(::^) :: a -> HList as -> HList (a :^ as)
data TypeList = TNil | (:^) Type TypeList
instance Show (HList TNil) where
show HNil = "HNil"
instance (Show a, Show (HList as)) => Show (HList (a:^as)) where
showsPrec p (x::^xs) = showParen (p>5)
$ showsPrec 6 x . ("::^"++) . showsPrec 5 xs
main :: IO ()
main = print ((2 :: Int) ::^ "bla" ::^ HNil)
Run Code Online (Sandbox Code Playgroud)
2::^"bla"::^HNil