Title here
Summary here
Enums in Idris
Our enum type ServerState has an underlying Int type.
The possible values for ServerState are defined as constants.
By implementing the Show interface, values of ServerState can be printed out or converted to strings.
If we have a value of type Int, we cannot pass it to transition - the compiler will complain about type mismatch. This provides some degree of compile-time type safety for enums.
transition emulates a state transition for a server; it takes the existing state and returns a new state.
module Main
import Data.Vect
%default total
public export
data ServerState : Type where
StateIdle : ServerState
StateConnected : ServerState
StateError : ServerState
StateRetrying : ServerState
serverStateToString : ServerState -> String
serverStateToString StateIdle = "idle"
serverStateToString StateConnected = "connected"
serverStateToString StateError = "error"
serverStateToString StateRetrying = "retrying"
instance Show ServerState where
show = serverStateToString
transition : ServerState -> ServerState
transition StateIdle = StateConnected
transition StateConnected = StateIdle
transition StateRetrying = StateIdle
transition StateError = StateError
main : IO ()
main = do
let ns = transition StateIdle
print ns
let ns2 = transition ns
print ns2To run the program, save the code in Main.idr and use the idris compiler to run it.
$ idris --exec main Main.idr
connected
idle