Safe Haskell | None |
---|
Construction and elimination of tuples in the object language
- data Tuple sig where
- Tup2 :: Tuple (a :-> (b :-> Full (a, b)))
- Tup3 :: Tuple (a :-> (b :-> (c :-> Full (a, b, c))))
- Tup4 :: Tuple (a :-> (b :-> (c :-> (d :-> Full (a, b, c, d)))))
- Tup5 :: Tuple (a :-> (b :-> (c :-> (d :-> (e :-> Full (a, b, c, d, e))))))
- Tup6 :: Tuple (a :-> (b :-> (c :-> (d :-> (e :-> (f :-> Full (a, b, c, d, e, f)))))))
- Tup7 :: Tuple (a :-> (b :-> (c :-> (d :-> (e :-> (f :-> (g :-> Full (a, b, c, d, e, f, g))))))))
- type family Sel1' a
- type family Sel2' a
- type family Sel3' a
- type family Sel4' a
- type family Sel5' a
- type family Sel6' a
- type family Sel7' a
- data Select a where
- Sel1 :: (Sel1 a b, Sel1' a ~ b) => Select (a :-> Full b)
- Sel2 :: (Sel2 a b, Sel2' a ~ b) => Select (a :-> Full b)
- Sel3 :: (Sel3 a b, Sel3' a ~ b) => Select (a :-> Full b)
- Sel4 :: (Sel4 a b, Sel4' a ~ b) => Select (a :-> Full b)
- Sel5 :: (Sel5 a b, Sel5' a ~ b) => Select (a :-> Full b)
- Sel6 :: (Sel6 a b, Sel6' a ~ b) => Select (a :-> Full b)
- Sel7 :: (Sel7 a b, Sel7' a ~ b) => Select (a :-> Full b)
- selectPos :: Select a -> Int
Construction
Expressions for constructing tuples
Tup2 :: Tuple (a :-> (b :-> Full (a, b))) | |
Tup3 :: Tuple (a :-> (b :-> (c :-> Full (a, b, c)))) | |
Tup4 :: Tuple (a :-> (b :-> (c :-> (d :-> Full (a, b, c, d))))) | |
Tup5 :: Tuple (a :-> (b :-> (c :-> (d :-> (e :-> Full (a, b, c, d, e)))))) | |
Tup6 :: Tuple (a :-> (b :-> (c :-> (d :-> (e :-> (f :-> Full (a, b, c, d, e, f))))))) | |
Tup7 :: Tuple (a :-> (b :-> (c :-> (d :-> (e :-> (f :-> (g :-> Full (a, b, c, d, e, f, g)))))))) |
Projection
These families (Sel1'
- Sel7'
) are needed because of the problem
described in:
http://emil-fp.blogspot.com/2011/08/fundeps-weaker-than-type-families.html
Expressions for selecting elements of a tuple
Sel1 :: (Sel1 a b, Sel1' a ~ b) => Select (a :-> Full b) | |
Sel2 :: (Sel2 a b, Sel2' a ~ b) => Select (a :-> Full b) | |
Sel3 :: (Sel3 a b, Sel3' a ~ b) => Select (a :-> Full b) | |
Sel4 :: (Sel4 a b, Sel4' a ~ b) => Select (a :-> Full b) | |
Sel5 :: (Sel5 a b, Sel5' a ~ b) => Select (a :-> Full b) | |
Sel6 :: (Sel6 a b, Sel6' a ~ b) => Select (a :-> Full b) | |
Sel7 :: (Sel7 a b, Sel7' a ~ b) => Select (a :-> Full b) |