10

假设我有一个Thing带有 state 属性的类型A | B | C，
并且合法的状态转换是A->B, A->C, C->A.

我可以写：

transitionToA :: Thing -> Maybe Thing

如果处于无法转换Nothing到.ThingA

但我想定义我的类型和转换函数，以便只能在适当的类型上调用转换。

一种选择是创建单独的类型AThing BThing CThing，但在复杂情况下似乎无法维护。

另一种方法是将每个状态编码为它自己的类型：

data A = A Thing
data B = B Thing
data C = C Thing

和

transitionCToA :: C Thing -> A Thing

这对我来说似乎更干净。但我突然想到，A、B、C 是函子，除了转换函数之外，所有的事物函数都可以被映射。

使用类型类，我可以创建如下内容：

class ToA t where  
    toA :: t -> A Thing

这似乎更清洁。

是否有其他可以在 Haskell 和 PureScript 中使用的首选方法？

4

4 回答 4

10

这是一种相当简单的方法，它使用（可能是幻像）类型参数来跟踪 aThing处于哪个状态：

{-# LANGUAGE DataKinds, KindSignatures #-}
-- note: not exporting the constructors of Thing
module Thing (Thing, transAB, transAC, transCA) where

data State = A | B | C
data Thing (s :: State) = {- elided; can even be a data family instead -}

transAB :: Thing A -> Thing B
transAC :: Thing A -> Thing C
transCA :: Thing C -> Thing A

transAB = {- elided -}
transAC = {- elided -}
transCA = {- elided -}
于 2015-08-17T21:44:08.727 回答
5

您可以按照 John 的建议使用类型类（在 PureScript 中可用）和幻像类型，但使用类型类作为路径类型的最终编码：

data A -- States at the type level
data B
data C

class Path p where
  ab :: p A B -- One-step paths
  ac :: p A C
  ca :: p C A
  trans :: forall a b c. p c b -> p b a -> p c a -- Joining paths
  refl :: forall a. p a a

现在您可以创建一种有效路径：

type ValidPath a b = forall p. (Path p) => p a b

roundTrip :: ValidPath A A
roundTrip = trans ca ac

路径只能通过使用您提供的单步路径来构建。

您可以编写实例来使用您的路径，但重要的是，任何实例都必须尊重类型级别的有效转换。

例如，这是一个计算路径长度的解释：

newtype Length = Length Int

instance pathLength :: Path Length where
  ab = Length 1
  ac = Length 1
  ca = Length 1
  trans (Length n) (Length m) = Length (n + m)
  refl = Length 0
于 2015-08-18T17:56:06.173 回答
2

由于您的目标是防止开发人员执行非法转换，您可能需要研究幻像类型。Phantom 类型允许您在不利用类型系统的更高级功能的情况下对类型安全的转换进行建模；因此，它们可以移植到多种语言。

这是您上述问题的 PureScript 编码：

foreign import data A :: *
foreign import data B :: *
foreign import data C :: *

data Thing a = Thing

transitionToA :: Thing C -> Thing A

当您具有两个不同状态不能转换到同一状态的属性时（除非所有状态都可以转换到该状态），幻像类型可以很好地模拟有效的状态转换。您可以通过使用类型类 ( class CanTransitionToA a where trans :: Thing a -> Thing A) 来解决此限制，但此时，您应该研究其他方法。

于 2015-08-18T14:18:33.653 回答
2

如果您想存储转换列表以便以后处理它，您可以执行以下操作：

{-# LANGUAGE DataKinds, GADTs, KindSignatures, PolyKinds #-}

data State = A | B | C
data Edge (a :: State) (b :: State) where
    EdgeAB :: Edge A B
    EdgeAC :: Edge A C
    EdgeCA :: Edge C A

data Domino (f :: k -> k -> *) (a :: k) (b :: k)  where
    I :: Domino f a a
    (:>>:) :: f a b -> Domino f b c -> Domino f a c

infixr :>>:

example :: Domino Edge A B
example = EdgeAC :>>: EdgeCA :>>: EdgeAB :>>: I

Path您可以通过为 编写连接函数将其转换为 的实例Domino：

{-# LANGUAGE FlexibleInstances #-}
instance Path (Domino Edge) where
    ab = EdgeAB :>>: I
    ac = EdgeAC :>>: I
    ca = EdgeCA :>>: I

    refl = I
    trans I es' = es'
    trans (e :>>: es) es' = e :>>: (es `trans` es')

事实上，这让我想知道 Hackage 是否已经有一个定义“索引幺半群”的包：

class IMonoid (m :: k -> k -> *) where
    imempty :: m a a
    imappend :: m a b -> m b c -> m a c

instance IMonoid (Domino e) where
    imempty = I
    imappend I es' = es'
    imappend (e :>>: es) es' = e :>>: (es `imappend` es')
于 2015-08-19T01:30:27.990 回答