Idris2: Dependent sum type discrimination

Question

This is probably very basic dependently typed programming problem, but I cannot find anything about it. The problem is this: "I have a bunch of messages that I may or may not have to handle depending on some configuration. How do I discriminate between the messages that I need to handle and the messages I don't need to handle at the type level".

So for example, I have some configuration and some messages.

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

I now want to be able to write something like this:

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

Is this, or something like this possible?

michaelmesser michaelmesser · Accepted Answer · 2021-05-22T00:49:36

One simple way to implement this without doing something like open unions is:

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

Idris2: Dependent sum type discrimination

1 Answers