blob: c34c1657e6b4fa6967c5f7cbe72c0126d14ba9d6 (
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
|
-- From the GHC users mailing list, 3/9/14
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
module BadSock where
import Data.Proxy
import GHC.Exts
data Message
data SocketType = Dealer | Push | Pull
data SocketOperation = Read | Write
data SockOp :: SocketType -> SocketOperation -> * where
SRead :: Foo 'Read sock => SockOp sock 'Read
SWrite :: Foo Write sock => SockOp sock Write
data Socket :: SocketType -> * where
Socket :: proxy sock
-> (forall op . Foo op sock => SockOp sock op -> Operation op)
-> Socket sock
type family Foo (op :: SocketOperation) :: SocketType -> Constraint where
Foo 'Read = Readable
Foo Write = Writable
type family Operation (op :: SocketOperation) :: * where
Operation 'Read = IO Message
Operation Write = Message -> IO ()
type family Readable (t :: SocketType) :: Constraint where
Readable Dealer = ()
Readable Pull = ()
type family Writable (t :: SocketType) :: Constraint where
Writable Dealer = ()
Writable Push = ()
{-
dealer :: Socket Dealer
dealer = undefined
push :: Socket Push
push = undefined
pull :: Socket Pull
pull = undefined
readSocket :: forall sock . Readable sock => Socket sock -> IO Message
readSocket (Socket _ f) = f (SRead :: SockOp sock 'Read)
-}
|
