问题描述
这可能是非常基本的依赖类型编程问题,但我找不到任何关于它的信息。问题是这样的:“我有一堆消息,我可能需要也可能不需要处理,这取决于某些配置。我如何区分我需要处理的消息和我不需要处理的消息?类型级别”。
例如,我有一些配置和一些消息。
record Configuration where
constructor MkConfiguration
handlesOpenClose: Bool
handlesWillSave: Bool
config : Configuration
config = MkConfiguration { openClose: True,willSave: False }
data Message = FileOpened -- Handle when openClose = True
| FileClosed -- Handle when openClose = True
| WillSave -- Handle when willSave = True
我现在希望能够写出这样的东西:
GetMessagesForConfig : Configuration -> Type
GetMessagesForConfig config = {-
config.openClose = true so FileOpened and FileClosed have to be handled,config.willSave = false so WillSave does not have to be handled
-}
MessagesForConfig : Type
MessagesForConfig = GetMessagesForConfig config
handleMessage : MessagesForConfig -> Response
handleMessage FileOpened = {- do something -}
handleMessage FileClosed = {- do something -}
handleMessage WillSave impossible
这或类似的事情可能吗?
解决方法
无需执行开放式联合之类的操作即可实现此目的的一种简单方法是:
data Message : (openClose : Bool) -> (willSave : Bool) -> Type where
FileOpened : Message True a
FileClosed : Message True a
WillSave : Message a True
handleMessage : Messages True False -> Response
handleMessage FileOpened = {- do something -}
handleMessage FileClosed = {- do something -}
handleMessage WillSave impossible