blob: e82d065d9a82d6184409c16550661c12dd5764f3 (
plain) (
blame)
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
|
{-# LANGUAGE Haskell2010 #-}
{-# LANGUAGE TypeOperators, GADTs, MultiParamTypeClasses, FlexibleContexts #-}
module TypeOperators where
data a :-: b
data (a :+: b) c
data a `Op` b
newtype (g `O` f) a = O { unO :: g (f a) }
class a <=> b
biO :: (g `O` f) a
biO = undefined
f :: (a ~ b) => a -> b
f = id
g :: (a ~ b, b ~ c) => a -> c
g = id
x :: ((a :-: a) <=> (a `Op` a)) => a
x = undefined
y :: (a <=> a, (a `Op` a) <=> a) => a
y = undefined
|
