Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- module Main
- data DoorState = DoorClosed | DoorOpen
- data DoorResult = OK | Jammed
- doorResult : DoorResult -> DoorState
- doorResult = \res => case res of
- OK => DoorOpen
- Jammed => DoorClosed
- data DoorCmd : (ty : Type) -> DoorState -> (ty -> DoorState) -> Type where
- Open : DoorCmd DoorResult DoorClosed doorResult
- Close : DoorCmd () DoorOpen (const DoorClosed)
- RingBell : DoorCmd () DoorClosed (const DoorClosed)
- Display : String -> DoorCmd () state (const state)
- Pure : (res : ty) -> DoorCmd ty (state_fn res) state_fn
- (>>=) : DoorCmd a state1 state2_fn ->
- ((res : a) -> DoorCmd b (state2_fn res) state3_fn) ->
- DoorCmd b state1 state3_fn
- doorProg : DoorCmd () DoorClosed (const DoorClosed)
- doorProg = do RingBell
- OK <- Open | Jammed => Display "Door Jammed"
- Display "Glad to be of service"
- Close
- {-
- - + Errors (1)
- `-- Chap14.idr line 27 col 14:
- When checking right hand side of Main.case block in doorProg at Chap14.idr:25:21 with expected type
- DoorCmd () (state2_fn OK) (\value => DoorClosed)
- When checking an application of constructor Main.>>=:
- Type mismatch between
- DoorCmd () DoorOpen (const DoorClosed) (Type of Close)
- and
- DoorCmd ()
- (const (state2_fn OK) _)
- (\value => DoorClosed) (Expected type)
- Specifically:
- Type mismatch between
- DoorOpen
- and
- state2_fn OK
- -}
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement