我有一个数据类型,它是一对可链接的函数。在伊德里斯这是
data Foo i o = MkFoo (i -> ty) (ty -> o)
我希望这在 Haskell 中意味着什么是相当明显的。这是一个广泛使用的构造,也许有名字?
你想ty
成为一个存在类型吗?
type Foo :: Cat Type
data Foo i o where
MkFoo :: (i -> ty) -> (ty -> o) -> Foo i o
^^ ^^
| |
does not appear in the result type
type Pro :: Type
type Pro = Type -> Type -> Type
type Procompose :: Pro -> Pro -> Pro
data Procompose pro2 pro1 іn out where
Procompose :: pro2 xx out -> pro1 іn xx -> Procompose pro2 pro1 іn out
这Foo
可以在以下方面进行定义
type Foo :: Cat Type
type Foo = Procompose (->) (->)
we quantify `ty` here because it's existential
|
vvvvvvvvv
pattern MkFoo :: forall іn out. () => forall ty. (іn -> ty) -> (ty -> out) -> Foo іn out
pattern MkFoo one two = Procompose two one
还有一个自由类的概念是一个类型对齐的列表;即可链接函数列表
type (~>) :: Cat (k -> Type)
type f ~> g = (forall x. f x -> g x)
type Quiver :: Type -> Type
type Quiver ob = ob -> ob -> Type
type Cat :: Type -> Type
type Cat ob = Quiver ob
infixr 5 :>>>
type FreeCategory :: Quiver ~> Cat
data FreeCategory cat a b where
Id :: FreeCategory cat a a
(:>>>) :: cat a b -> FreeCategory cat b c -> FreeCategory cat a c
可以写成长度为 2 的类型对齐列表:
type Foo :: Cat Type
type Foo = FreeCategory (->)
we quantify `ty` here because it's existential
|
vvvvvvvvv
pattern MkFoo :: forall іn out. () => forall ty. (іn -> ty) -> (ty -> out) -> Foo іn out
pattern MkFoo one two = one :>>> two :>>> Id
自由类别也可以定义为Free2 Category
通过将Category
类传递给Free2
.. 有点漫不经心的答案
type (~~>) :: Cat (k1 -> k2 -> Type)
type f ~~> g = (forall x. f x ~> g x)
type Free2 :: (Cat ob -> Constraint) -> Quiver ob -> Cat ob
type Free2 cls cat a b = (forall xx. cls xx => (cat ~~> xx) -> xx a b)
type FreeCategory :: Quiver ~> Cat
type FreeCategory cat a b = Free2 Category cat a b
本文收集自互联网,转载请注明来源。
如有侵权,请联系 [email protected] 删除。
我来说两句