blob: d4cfa1e275cee060fd175ee073087e292f1b02ac (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
|
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns -fwarn-overlapping-patterns #-}
module T3927b where
import Data.Kind (Type, Constraint)
import Data.Proxy
data Message
data SocketType = Dealer | Push | Pull
data SocketOperation = Read | Write
type family Restrict (a :: SocketOperation) (as :: [SocketOperation]) :: Constraint where
Restrict a (a ': as) = ()
Restrict x (a ': as) = Restrict x as
Restrict x '[] = ("Error!" ~ "Tried to apply a restricted type!")
type family Implements (t :: SocketType) :: [SocketOperation] where
Implements Dealer = ['Read, Write]
Implements Push = '[Write]
Implements Pull = '[ 'Read]
data SockOp :: SocketType -> SocketOperation -> Type where
SRead :: SockOp sock 'Read
SWrite :: SockOp sock Write
data Socket :: SocketType -> Type where
Socket :: proxy sock
-> (forall op . Restrict op (Implements sock) => SockOp sock op -> Operation op)
-> Socket sock
type family Operation (op :: SocketOperation) :: Type where
Operation 'Read = IO Message
Operation Write = Message -> IO ()
class Restrict 'Read (Implements t) => Readable t where
readSocket :: Socket t -> Operation 'Read
readSocket (Socket _ f) = f (SRead :: SockOp t 'Read)
instance Readable Dealer
type family Writable (t :: SocketType) :: Constraint where
Writable Dealer = ()
Writable Push = ()
dealer :: Socket Dealer
dealer = Socket (Proxy :: Proxy Dealer) f
where
f :: Restrict op (Implements Dealer) => SockOp Dealer op -> Operation op
f SRead = undefined
f SWrite = undefined
push :: Socket Push
push = Socket (Proxy :: Proxy Push) f
where
f :: Restrict op (Implements Push) => SockOp Push op -> Operation op
f SWrite = undefined
-- Seeing that this pattern match is exhaustive
-- requires a reasonably vigorous effort on given
-- superclass expansion.
pull :: Socket Pull
pull = Socket (Proxy :: Proxy Pull) f
where
f :: Restrict op (Implements Pull) => SockOp Pull op -> Operation op
f SRead = undefined
foo :: IO Message
foo = readSocket dealer
|
