时间戳

首页 > 解决方案 > 这个 Haskell 代码在多大程度上满足了这个规范？

haskell - 这个 Haskell 代码在多大程度上满足了这个规范？

问题描述

清单 1是来自论文的 Haskell 类签名和实例。如果一个人在给定的房子或给定的房间中，该isIn person house函数应该返回 true。

清单 1

class CONTAINMENT container for where
 isIn :: for -> container -> Bool


instance CONTAINMENT House Person where
 isIn person house =
         (container person = house) || isIn (container person) house

的定义中有错误isIn person house，我希望在这篇文章中忽略这些错误。

相反，我希望将清单 1与下面的文本描述（来自论文）一起考虑作为规范（即说明符意图的合理表示）。

文字说明

isIn 的公理使用 Person (person) 和 House (house) 类型的个体变量，并声明如果房子包含她，或者递归地，如果房子包含包含她。为了说明这一点，我使用状态表示作为标记的字段容器，这里假设是为人员类型定义的。

从规范看来：

清单 2

{-# LANGUAGE MultiParamTypeClasses #-}
    data Room  = Room Int deriving (Show,Eq)
    data Rooms = Rooms  [Room]  deriving (Show,Eq)

    data House  =  House Int Rooms deriving (Show,Eq)
    data Person = Person {container :: House }  deriving (Show,Eq)

    getRooms::House->Rooms
    getRooms (House n rooms) = rooms

    getHouse::Person->House
    getHouse p = container p 


    getRoom::House->Room
    getRoom (House n (Rooms (x:xs)))  = x


    class CONTAINMENT container for where
     isIn :: for -> container -> Bool

    instance CONTAINMENT House  Person where
     isIn  person   (House n (Rooms rooms)) = (container person) ==  (House n (Rooms rooms)) ||  isIn  person  (getRooms (House n (Rooms rooms)))

    instance CONTAINMENT Rooms Person where
     isIn person (Rooms []) = False
     isIn person (Rooms (room:rooms)) = (room == getRoom(getHouse(person))) ||  isIn person (Rooms rooms)

    r1 = Room 1
    r2 = Room 2
    h1 = House 1 (Rooms [])
    h2 = House 2 (Rooms [r1])
    h3 = House 3 (Rooms [r1,r2])
    p1 = Person {container = h1}
    p2 = Person  {container = h2}
    p3 = Person  {container = h3}
    personInHoseNoRooms = isIn p1 h1
    personInHoseNoRoomsNotIn = isIn p1 h2
    personInRoomInHouse = isIn p2 h2
    personIn2ndRoomInHouse = isIn p3 h3

该代码似乎与规范大体一致。但是，我看到一些问题：

  1. 如果 disjunct in 的第一个参数isIn为假，而第二个参数为真，那么我们得到的信息是一个人在一个房间里，但不在包含该房间的房子里。这在我看来是一个逻辑矛盾，一个人不在房子 A，而是在房子 A 的房间里。这可能是我对规范或编码的理解有误。
  2. 递归一词通常适用于单一日期类型，但在重载isIn后适用于Houseand Rooms，其中House结构包含Rooms. 同样，这可能是我的一个错误。
  3. 就目前而言，没有提到全球唯一的房间标识符。相同的房间号可能出现在不同的房屋中，这可能会产生模棱两可的结果。我认为这些Room-House-Person关系存在一些更深层次的问题，我无法清楚地表达出来。

问题

  1. 关于如何克服上述问题的任何编码建议。
  2. 或者，实际上是否可以实施规范？

标签： haskellrecursionspecifications

解决方案

通过一些最小的更改，至少它可以在 GHC 中编译：

{-# LANGUAGE MultiParamTypeClasses #-}

data Room  = Room Int deriving (Show,Eq)
data Rooms = Rooms [Room] deriving (Show,Eq)

data House  =  House Int Rooms deriving (Show,Eq)
data Person = Person {container :: House }  deriving (Show,Eq)

getRooms :: House -> Rooms
getRooms (House n rooms) = rooms

getHouse :: Person -> House
getHouse p = container p 

getRoom :: House -> Room
getRoom (House n (Rooms (x:xs)))  = x

class Containment c f where
 isIn :: f -> c -> Bool

instance Containment House  Person where
 isIn person (House n (Rooms rooms)) = (container person) ==  (House n (Rooms rooms)) || isIn person (getRooms (House n (Rooms rooms)))

instance Containment Rooms Person where
 isIn person (Rooms []) = False
 isIn person (Rooms (room:rooms)) = (room == getRoom(getHouse(person))) ||  isIn person (Rooms rooms)

r1 = Room 1
r2 = Room 2
h1 = House 1 (Rooms [])
h2 = House 2 (Rooms [r1])
h3 = House 3 (Rooms [r1,r2])
p1 = Person {container = h1}
p2 = Person {container = h2}
p3 = Person {container = h3}
personInHoseNoRooms      = isIn p1 h1
personInHoseNoRoomsNotIn = isIn p1 h2
personInRoomInHouse      = isIn p2 h2
personIn2ndRoomInHouse   = isIn p3 h3

所以关于你的问题，是的，它可以在 Haskell 中实现。

关于声明：

如果房子包含她，或者递归地，如果房子包含一个包含她的容器（例如，一个房间）。

我同意你的说法，这recursively不是正确的词，应该是transitively。

推荐阅读