是否有可能在 haskell中構造一種將一種型別映射a到同一種型別的型別級別標識?a
以下是一些非答案:
type One :: * -> *
newtype One a = One {unOne :: a}
-- >>> :kind! 'One
-- 'One :: a -> One a -- not the identity
-- = 'One
type family Id a where -- *pointwise* identity, not a function (can't not apply it)
Id a = a
uj5u.com熱心網友回復:
目前型別語言是一階的,這意味著無法匹配的功能Id必須完全飽和:Haskell 中的高階型別級編程。
已經接受了解決此問題的建議:不飽和型別族。
根據這個提議,我們區分 和 的One :: Type -> Type種類Id :: k -> k;One可匹配和不可匹配Id:
One :: Type -> @M Type
Id :: k -> @U k
我們將能夠將無法匹配的型別級函式作為引數傳遞:
data Foo :: (Type -> @U Type) -> Type
data Foo f = MkFoo (f Int) (f Bool) (f Char)
foo :: Foo Id
foo = MkFoo 10 False 'a'
這將允許您構建適當的恒等函子、函子組合和分類小工具。
type Functor :: (s -> @m t) -> Constraint
class (Category (Source f), Category (Target f))
=> Functor (f :: s -> @m t) where
type Source (f :: s -> @m t) :: Cat s
type Target (f :: s -> @m t) :: Cat t
fmap :: Source f a a' -> Target f (f a) (f a')
type IdFunctor :: Cat ob -> ob -> ob
type IdFunctor cat a = a
instance Category @ob cat => Functor (IdFunctor @ob cat) where
type Source (IdFunctor cat) = cat
type Target (IdFunctor cat) = cat
fmap :: cat a a' -> cat a a'
fmap = id
轉載請註明出處,本文鏈接:https://www.uj5u.com/houduan/434050.html
上一篇:搜索二叉樹并回傳值的級別
