cluss (empty) → 0.1

raw patch · 4 files changed

+475/−0 lines, 4 filesdep +basesetup-changed

Dependencies added: base

Files

LICENSE +28/−0
Setup.hs +2/−0
cluss.cabal +57/−0
src/Type/Cluss.hs +388/−0

+ LICENSE view

@@ -0,0 +1,28 @@+Copyright (c) 2014, Yusuke Matsushita+All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++* Redistributions of source code must retain the above copyright notice, this+  list of conditions and the following disclaimer.++* Redistributions in binary form must reproduce the above copyright notice,+  this list of conditions and the following disclaimer in the documentation+  and/or other materials provided with the distribution.++* Neither the name of Cluss nor the names of its+  contributors may be used to endorse or promote products derived from+  this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"+AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR+SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER+CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,+OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.+

+ Setup.hs view

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

+ cluss.cabal view

@@ -0,0 +1,57 @@+name: cluss
+category: type system, constraints
+version: 0.1
+license: BSD3
+license-file: LICENSE
+cabal-version: >= 1.10
+tested-with: GHC==7.8.3
+author: Yusuke Matsushita
+maintainer: Yusuke Matsushita <y.skm24t@gmail.com>
+stability: provinsional
+homepage: https://github.com/Kinokkory/cluss
+bug-reports: https://github.com/Kinokkory/cluss/issues
+copyright: Copyright (C) 2014 Yusuke Matsushita
+synopsis: Simple Alternative to Type Classes
+description:
+    A /cluss/ enables you to achieve /function overloading/, or ad-hoc polymorphism,
+    without creating a new type class.
+    .
+    In order to give ad-hoc polymorphism to a type variable @a@,
+    you simply use @In@ with a list of "type patterns" like @In [Type T, ...] a@,
+    which indicates that the type matches some of the patterns;
+    which is analogous to a type class indicating that a type matches some of its "instances".
+    The constraint @In [Type T, ...] a@ is what we call a "cluss".
+    .
+    Cluss instances are /closed/ and cluss methods are /open/,
+    unlike type classes, whose instances are open and whose methods are closed.
+    .
+    Clusses can easily be used in a nested way,
+    and can even be /recursive/, just like recursive type classes,
+    and therefore clusses are expressive enough to imitate Haskell-98-style type classes.
+    .
+    More information can be found in the Haddock or the comments in the source code.
+
+build-type: Simple
+
+source-repository head
+    type: git
+    location: git@github.com:Kinokkory/cluss.git
+
+library
+    hs-source-dirs: src
+    default-language: Haskell2010
+    other-extensions:
+        TypeFamilies
+        PolyKinds
+        DataKinds
+        TypeOperators
+        MultiParamTypeClasses
+        FlexibleInstances
+        ScopedTypeVariables
+        UndecidableInstances
+        FlexibleContexts
+        ConstraintKinds
+        RankNTypes
+    build-depends: base == 4.*
+    exposed-modules: Type.Cluss
+    ghc-options: -Wall

+ src/Type/Cluss.hs view

@@ -0,0 +1,388 @@+{-# LANGUAGE TypeFamilies, PolyKinds, DataKinds, TypeOperators, MultiParamTypeClasses, FlexibleInstances, ScopedTypeVariables, UndecidableInstances, FlexibleContexts, ConstraintKinds, RankNTypes #-}
+
+module Type.Cluss (
+    -- * Clusses
+    In(..)
+
+    -- * Type Patterns
+    {-| Type patterns are used in the type list (first parameter) of 'In'.
+        Each type pattern corresponds to the head of an instance declaration for a type class, namely, @instance ... where@. -}
+  , Type, type (<|), Unary, Binary, Ternary, Quaternary, Quinary, Senary
+
+    -- * Instance Products
+  , AllOf, AllOf'(..)
+
+    -- * Constraint Combinators
+    {-| Constraint combinators are used in the second parameter of '<|', 'Unary', 'Binary', ..., 'Senary'.
+        Note that each combinator is kind-polymorphic. -}
+
+    -- ** Basic Combinators
+  , This, Pure, Is
+
+    -- ** Combinators for Overlaying Contraints
+  , type (>+<), type (>++<), type (>+++<), type (>++++<), type (>+++++<), type (>++++++<)
+
+    -- ** Combinators for Bonding Contraints
+  , type (>|<), type (>||<), type (>|||<), type (>||||<), type (>|||||<)
+
+    -- * Helpers
+
+    -- ** Helpers for Identical Constructors
+  , AllOfI, AllOfI', andI, andI1, andI2, andI3, andI4, andI5, andI6, noneI, projI
+
+    -- ** Helpers for Function Constructors
+  , AllOfF, AllOfF', andF, andF1, andF2, andF3, andF4, andF5, andF6, noneF, projF
+
+    -- * Examples
+
+    -- ** Example1: Hello
+    -- $hello
+
+    -- ** Example2: Printf
+    -- $printf
+
+    -- ** Example3: Monad
+    -- $monad
+
+    ) where
+
+import Prelude hiding (and)
+import GHC.Exts
+
+-- $hello
+-- Let's begin with a basic example.
+--
+-- >type Hellos = [
+-- >    Type String,
+-- >    Type Int,
+-- >    Type Double,
+-- >    Unary [] Show,
+-- >    Quaternary (,,,) (This >|< This >||< This >|||< This)]
+-- >hello :: In Hellos a => a -> String
+-- >hello = projF (
+-- >    (\s -> "hello, " ++ s) `andF`
+-- >    (\n -> "Mr. " ++ show n) `andF`
+-- >    (\x -> show (x / 2) ++ " times two") `andF`
+-- >    (\xs -> concatMap ((++", ") . show) xs ++ "period") `andF1`
+-- >    (\(x,y,z,w) ->
+-- >        hello x ++ " and " ++ hello y ++ " and " ++
+-- >        hello z ++ " and " ++ hello w) `andF4`
+-- >    noneF :: AllOfF Hellos String)
+-- >
+-- >main = putStrLn $
+-- >    hello ("world", 42 :: Int, 3.14 :: Double, [True, False])
+--
+-- This is the result.
+--
+-- > hello, world and Mr. 42 and 1.57 times two and True, False, period
+
+-- $printf
+-- With a recursive cluss,
+-- you can easily make a function that can take a variable number of arguments.
+-- The function below is a simplified C-style printf.
+--
+-- >type Printfs = [Binary (->) (Show >|< This), Type String]
+-- >printf :: In Printfs a => String -> a
+-- >printf s = projI (
+-- >    (\x -> printf (go s (show x))) `andI2`
+-- >    s `andI`
+-- >    noneI :: AllOfI Printfs)
+-- >  where
+-- >    go ('@' : cs) t = t ++ cs
+-- >    go (c : cs) t = c : go cs t
+-- >    go [] t = error "there is no '@' any more!"
+-- >
+-- >main = putStrLn $
+-- >    printf "@ good @ and @" 12 "men" True
+--
+-- This is the result.
+--
+-- >12 good "men" and True
+
+-- $monad
+-- Here is a more complex example.
+-- When the type of a "cluss method" is complex, you generally have to create newtypes (like Bind and Return below).
+--
+-- >type Monads = [Type [], Unary (->) Pure, Unary (,) Monoid, Unary Wrap This]
+-- >newtype Wrap m a = Wrap {unWrap :: m a}
+-- >newtype Bind a b m = Bind {unBind :: m a -> (a -> m b) -> m b}
+-- >newtype Return a m = Return {unReturn :: a -> m a}
+-- >bind :: In Monads m => m a -> (a -> m b) -> m b
+-- >bind = unBind $ proj (
+-- >    Bind (\m k -> concatMap k m) `And`
+-- >    Bind (\m k e -> k (m e) e) `And1`
+-- >    Bind (\(a,x) k -> let (a',x') = k x in (a<>a',x')) `And1`
+-- >    Bind (\m k -> Wrap (unWrap m `bind` (unWrap . k))) `And1`
+-- >    None :: AllOf Monads (Bind a b))
+-- >return' :: In Monads m => a -> m a
+-- >return' = unReturn $ proj (
+-- >    Return (: []) `And`
+-- >    Return const `And1`
+-- >    Return ((,) mempty) `And1`
+-- >    Return (Wrap . return') `And1`
+-- >    None :: AllOf Monads (Return a))
+-- >infixl 1 `bind`
+-- >
+-- >main = print $
+-- >    return' 1 `bind` replicate 3 `bind` (\n -> [n .. n+4])
+--
+-- This is the result.
+--
+-- >[1,2,3,4,5,1,2,3,4,5,1,2,3,4,5]
+
+data Look_At_Head
+data Look_At_Tail a
+data No_I_Don't_Have_That
+
+-- | The empty type @Type a@ is a type pattern.
+-- For example, the type pattern @Type Int@ corresponds to @instance C Int where ...@ (@C@ is a type class).
+-- Note that the type variable @a@ can be of any kind.
+data Type (a :: k)
+-- | The empty type @a <| p@ is a type pattern,
+-- where @a@ is a type constructor, and @p@ is a constraint function for the type variables for the constructor 'a'.
+-- For example, the type pattern @[] <| Show@ corresponds to @instance (Show a) => C [a] where ...@ (@C@ is a type class).
+--
+-- You can replace any of 'Unary', 'Binary', ..., 'Senary' with '<|',
+-- but you can sometimes save the effort of annotating kinds
+-- using 'Unary', 'Binary', ..., 'Senary' instead of '<|',
+-- especially when using @PolyKinds@ extension,
+-- because kinds of parameters are restricted in 'Unary', 'Binary', ..., 'Senary'.
+data (a :: k) <| (p :: l)
+-- | @a '<|' p@, with @a@ being of the kind @i -> k@ and @p@, @i -> 'Constraint'@.
+type Unary (a :: i -> k) (p :: i -> Constraint) = a <| p
+-- | @a '<|' p@, with @a@ being of the kind @i -> i' -> k@ and @p@, @i -> i' -> 'Constraint'@.
+type Binary (a :: i -> i' -> k) (p :: i -> i' -> Constraint) = a <| p
+-- | @a '<|' p@, with @a@ being of the kind @i -> i' -> i'' -> k@ and @p@, @i -> i' -> i'' -> 'Constraint'@.
+type Ternary (a :: i -> i' -> k) (p :: i -> i' -> i'' -> Constraint) = a <| p
+-- | @a '<|' p@, with @a@ being of the kind @i -> i' -> i'' -> i''' -> k@ and @p@, @i -> i' -> i'' -> i''' -> 'Constraint'@.
+type Quaternary (a :: i -> i' -> i'' -> i''' -> k) (p :: i -> i' -> i'' -> i''' -> Constraint) = a <| p
+-- | @a '<|' p@, with @a@ being of the kind @i -> i' -> i'' -> i''' -> i'''' -> k@ and @p@, @i -> i' -> i'' -> i''' -> i'''' -> 'Constraint'@.
+type Quinary (a :: i -> i' -> i'' -> i''' -> i'''' -> k) (p :: i -> i' -> i'' -> i''' -> i'''' -> Constraint) = a <| p
+-- | @a '<|' p@, with @a@ being of the kind @i -> i' -> i'' -> i''' -> i'''' -> i''''' -> k@ and @p@, @i -> i' -> i'' -> i''' -> i'''' -> i''''' -> 'Constraint'@.
+type Senary (a :: i -> i' -> i'' -> i''' -> i'''' -> i''''' -> k) (p :: i -> i' -> i'' -> i''' -> i'''' -> i''''' -> Constraint) = a <| p
+
+-- | 'This' creates a recursion.
+-- In other words, 'This' will work as @'In' as@ itself
+-- when used in the type list (first parameter) @as@ of 'In',
+-- combined with 'Type', '<|', 'Unary', 'Binary', ..., 'Senary',
+-- '>+<', '>++<', ..., '>++++++<',
+-- '>|<', '>||<', ..., '>|||||<'.
+--
+-- Note that 'This' won't be expanded into @'In' as@
+-- if the condition described above is not satisfied.
+-- Internally, the expansion is executed by 'Modify', 'Modify2', ..., 'Modify6'.
+--
+-- The instance of 'This' itself can't be created
+-- since the context @True~False@ will never be satisfied.
+--
+-- There is no predetermined limit of recursion depth,
+-- but GHC has a fixed-depth recursion stack for safety,
+-- so you may need to increase the stack depth with @-fcontext-stack=N@.
+class True ~ False => This (a :: k)
+-- | @'Pure' a@ is equivalent to the empty constraint @()@.
+--
+-- >Pure a == ()
+class Pure (a :: i)
+instance Pure a
+-- |
+-- >(p >+< q) a == (p a, q a)
+class (p a, q a) => (>+<) p q a
+instance (p a, q a) => (>+<) p q a
+-- |
+-- >(p >++< q) a b == (p a b, q a b)
+class (p a b, q a b) => (>++<) p q a b
+instance (p a b, q a b) => (>++<) p q a b
+-- |
+-- >(p >+++< q) a b c == (p a b c, q a b c)
+class (p a b c, q a b c) => (>+++<) p q a b c
+instance (p a b c, q a b c) => (>+++<) p q a b c
+-- |
+-- >(p >++++< q) a b c d == (p a b c d, q a b c d)
+class (p a b c d, q a b c d) => (>++++<) p q a b c d
+instance (p a b c d, q a b c d) => (>++++<) p q a b c d
+-- |
+-- >(p >+++++< q) a b c d e == (p a b c d e, q a b c d e)
+class (p a b c d e, q a b c d e) => (>+++++<) p q a b c d e
+instance (p a b c d e, q a b c d e) => (>+++++<) p q a b c d e
+-- |
+-- >(p >++++++< q) a b c d e f == (p a b c d e f, q a b c d e f)
+class (p a b c d e f, q a b c d e f) => (>++++++<) p q a b c d e f
+instance (p a b c d e f, q a b c d e f) => (>++++++<) p q a b c d e f
+-- |
+-- >(p >|< q) a b == (p a, q b)
+class (p a, q b) => (>|<) p q a b
+instance (p a, q b) => (>|<) p q a b
+-- |
+-- >(p >||< q) a b c == (p a b, q c)
+class (p a b, q c) => (>||<) p q a b c
+instance (p a b, q c) => (>||<) p q a b c
+-- |
+-- >(p >|||< q) a b c d == (p a b c, q d)
+class (p a b c, q d) => (>|||<) p q a b c d
+instance (p a b c, q d) => (>|||<) p q a b c d
+-- |
+-- >(p >||||< q) a b c d e == (p a b c d, q e)
+class (p a b c d, q e) => (>||||<) p q a b c d e
+instance (p a b c d, q e) => (>||||<) p q a b c d e
+-- |
+-- >(p >|||||< q) a b c d e f == (p a b c d e, q f)
+class (p a b c d e, q f) => (>|||||<) p q a b c d e f
+instance (p a b c d e, q f) => (>|||||<) p q a b c d e f
+
+-- |
+-- >(Is a) b == (a ~ b)
+type Is a b = a ~ b
+
+infixl 7 <|
+infixl 8 >|<, >||<, >|||<, >||||<, >|||||<
+infixl 9 >+<, >++<, >+++<, >++++<, >+++++<, >++++++<
+
+type family Where (as :: [*]) (a :: k) :: * where
+    Where (Type a ': as) a = Look_At_Head
+    Where (a <| p ': as) (a b) = Look_At_Head
+    Where (a <| p ': as) (a b c) = Look_At_Head
+    Where (a <| p ': as) (a b c d) = Look_At_Head
+    Where (a <| p ': as) (a b c d e) = Look_At_Head
+    Where (a <| p ': as) (a b c d e f) = Look_At_Head
+    Where (a <| p ': as) (a b c d e f g) = Look_At_Head
+    Where (b ': as) a = Look_At_Tail (Where as a)
+    Where '[] a = No_I_Don't_Have_That
+
+type family Modify (this :: k -> Constraint) (a :: k -> Constraint) :: k -> Constraint where
+    Modify this This = this
+    Modify this (s >+< s') = Modify this s >+< Modify this s'
+    Modify this s = s
+type family Modify2 (this :: k -> Constraint) (a :: k -> k' -> Constraint) :: k -> k' -> Constraint where
+    Modify2 this (s >++< s') = Modify2 this s >++< Modify2 this s'
+    Modify2 this (s >|< s') = Modify this s >|< Modify this s'
+    Modify2 this s = s
+type family Modify3 (this :: k -> Constraint) (a :: k -> k' -> k'' -> Constraint) :: k -> k' -> k'' -> Constraint where
+    Modify3 this (s >+++< s') = Modify3 this s >+++< Modify3 this s'
+    Modify3 this (s >||< s') = Modify2 this s >||< Modify this s'
+    Modify3 this s = s
+type family Modify4 (this :: k -> Constraint) (a :: k -> k' -> k'' -> k''' -> Constraint) :: k -> k' -> k'' -> k''' -> Constraint where
+    Modify4 this (s >++++< s') = Modify4 this s >++++< Modify4 this s'
+    Modify4 this (s >|||< s') = Modify3 this s >|||< Modify this s'
+    Modify4 this s = s
+type family Modify5 (this :: k -> Constraint) (a :: k -> k' -> k'' -> k''' -> k'''' -> Constraint) :: k -> k' -> k'' -> k''' -> k'''' -> Constraint where
+    Modify5 this (s >+++++< s') = Modify5 this s >+++++< Modify5 this s'
+    Modify5 this (s >||||< s') = Modify4 this s >||||< Modify this s'
+    Modify5 this s = s
+type family Modify6 (this :: k -> Constraint) (a :: k -> k' -> k'' -> k''' -> k'''' -> k''''' -> Constraint) :: k -> k' -> k'' -> k''' -> k'''' -> k''''' -> Constraint where
+    Modify6 this (s >++++++< s') = Modify6 this s >++++++< Modify6 this s'
+    Modify6 this (s >|||||< s') = Modify5 this s >|||||< Modify this s'
+    Modify6 this s = s
+
+-- |@'AllOf' as f@ is a tuple that contains values of the type @f a@,
+-- where @a@ can be any type that satisfies @In as a@.
+-- Each value corresponds to each type pattern,
+-- and the values in @'AllOf' as f@ must be in the same order as the type patterns in @as@.
+-- 'And', 'And1', 'And2', ..., 'And6' are used to combine the values
+-- and 'None' must be added at the end.
+-- You have to use 'And' for @'Type' a@,
+-- 'And1' for @'Unary' a p@, 'And2' for  @'Binary' a p@,
+-- ..., 'And6' for @'Senary' a p@.
+type AllOf as = AllOf' as as
+data family AllOf' (ts :: [*]) (as :: [*]) (f :: k -> *)
+data instance AllOf' ts (Type a ': as) f = And (f a) (AllOf' ts as f)
+data instance AllOf' ts (Unary a p ': as) f = And1 (forall b. Modify (In ts) p b => f (a b)) (AllOf' ts as f)
+data instance AllOf' ts (Binary a p ': as) f = And2 (forall b c. Modify2 (In ts) p b c => f (a b c)) (AllOf' ts as f )
+data instance AllOf' ts (Ternary a p ': as) f = And3 (forall b c d. Modify3 (In ts) p b c d => f (a b c d)) (AllOf' ts as f)
+data instance AllOf' ts (Quaternary a p ': as) f = And4 (forall b c d e. Modify4 (In ts) p b c d e => f (a b c d e)) (AllOf' ts as f)
+data instance AllOf' ts (Quinary a p ': as) f = And5 (forall b c d e f'. Modify5 (In ts) p b c d e f' => f (a b c d e f')) (AllOf' ts as f)
+data instance AllOf' ts (Senary a p ': as) f = And6 (forall b c d e f' g. Modify6 (In ts) p b c d e f' g => f (a b c d e f' g)) (AllOf' ts as f)
+data instance AllOf' ts '[] f = None
+
+infixr 0 `And`, `And1`, `And2`, `And3`, `And4`, `And5`, `And6`
+
+-- | @'In' as@ is a /cluss/, where @as@ is a list of type patterns.
+-- Normally, @as@ is concrete and does not contain any type variables, like @In [Binary (->) (Show >|< This), Type String] a@.
+--
+-- When @a@ satisfies @In as a@, you can use the method @'proj' :: 'AllOf' as f -> f a@.
+--
+-- Clusses call for some language extensions. Basically, this language pragma will do.
+--
+-- >{-# LANGUAGE DataKinds, FlexibleContexts, TypeOperators #-}
+--
+-- Internally, "type pattern matching" is executed by 'Where', a closed type family, which cannot check if a type satisfies a constraint.
+-- If @as@ has many type patterns that can match @a@, only the first one matches @a@.
+class In (as :: [*]) (a :: k) where
+    proj :: AllOf as f -> f a
+instance In' (Where as a) as as a => In as a where
+    proj = proj' (undefined :: Where as a)
+class In' (n :: *) (ts :: [*]) (as :: [*]) (a :: k) where
+    proj' :: n -> AllOf' ts as f -> f a
+instance In' Look_At_Head ts (Type a ': as) a where
+    proj' _ (And x _) = x
+instance Modify (In ts) p b => In' Look_At_Head ts (a <| p ': as) (a b) where
+    proj' _ (And1 x _) = x
+instance Modify2 (In ts) p b c => In' Look_At_Head ts (a <| p ': as) (a b c) where
+    proj' _ (And2 x _) = x
+instance Modify3 (In ts) p b c d => In' Look_At_Head ts (a <| p ': as) (a b c d) where
+    proj' _ (And3 x _) = x
+instance Modify4 (In ts) p b c d e => In' Look_At_Head ts (a <| p ': as) (a b c d e) where
+    proj' _ (And4 x _) = x
+instance Modify5 (In ts) p b c d e f => In' Look_At_Head ts (a <| p ': as) (a b c d e f) where
+    proj' _ (And5 x _) = x
+instance Modify6 (In ts) p b c d e f g => In' Look_At_Head ts (a <| p ': as) (a b c d e f g) where
+    proj' _ (And6 x _) = x
+instance In' n ts as a => In' (Look_At_Tail n) ts (Type (b :: k) ': as) (a :: k) where
+    proj' _ (And _ xs) = proj' (undefined :: n) xs
+instance In' n ts as a => In' (Look_At_Tail n) ts ((b :: i -> k) <| (p :: i -> Constraint) ': as) (a :: k) where
+    proj' _ (And1 _ xs) = proj' (undefined :: n) xs
+instance In' n ts as a => In' (Look_At_Tail n) ts ((b :: i -> i' -> k) <| (p :: i -> i' -> Constraint) ': as) (a :: k) where
+    proj' _ (And2 _ xs) = proj' (undefined :: n) xs
+instance In' n ts as a => In' (Look_At_Tail n) ts ((b :: i -> i' -> i'' -> k) <| (p :: i -> i' -> i'' -> Constraint) ': as) (a :: k) where
+    proj' _ (And3 _ xs) = proj' (undefined :: n) xs
+instance In' n ts as a => In' (Look_At_Tail n) ts ((b :: i -> i' -> i'' -> i''' -> k) <| (p :: i -> i' -> i'' -> i''' -> Constraint) ': as) (a :: k) where
+    proj' _ (And4 _ xs) = proj' (undefined :: n) xs
+instance In' n ts as a => In' (Look_At_Tail n) ts ((b :: i -> i' -> i'' -> i''' -> i'''' -> k) <| (p :: i -> i' -> i'' -> i''' -> i'''' -> Constraint) ': as) (a :: k) where
+    proj' _ (And5 _ xs) = proj' (undefined :: n) xs
+instance In' n ts as a => In' (Look_At_Tail n) ts ((b :: i -> i' -> i'' -> i''' -> i'''' -> i''''' -> k) <| (p :: i -> i' -> i'' -> i''' -> i'''' -> i''''' -> Constraint) ': as) (a :: k) where
+    proj' _ (And6 _ xs) = proj' (undefined :: n) xs
+
+newtype Id a = Id {unId :: a}
+type AllOfI as = AllOfI' as as
+type AllOfI' ts as = AllOf' ts as Id
+andI :: a -> AllOfI' ts as -> AllOfI' ts (Type a ': as)
+andI x y = And (Id x) y
+andI1 :: (forall b. Modify (In ts) p b => a b) -> AllOfI' ts as -> AllOfI' ts (a <| p ': as)
+andI1 x y = And1 (Id x) y
+andI2 :: (forall b c. Modify2 (In ts) p b c => a b c) -> AllOfI' ts as -> AllOfI' ts (a <| p ': as)
+andI2 x y = And2 (Id x) y
+andI3 :: (forall b c d. Modify3 (In ts) p b c d => a b c d) -> AllOfI' ts as -> AllOfI' ts (a <| p ': as)
+andI3 x y = And3 (Id x) y
+andI4 :: (forall b c d e. Modify4 (In ts) p b c d e => a b c d e) -> AllOfI' ts as -> AllOfI' ts (a <| p ': as)
+andI4 x y = And4 (Id x) y
+andI5 :: (forall b c d e f. Modify5 (In ts) p b c d e f => a b c d e f) -> AllOfI' ts as -> AllOfI' ts (a <| p ': as)
+andI5 x y = And5 (Id x) y
+andI6 :: (forall b c d e f g. Modify6 (In ts) p b c d e f g => a b c d e f g) -> AllOfI' ts as -> AllOfI' ts (a <| p ': as)
+andI6 x y = And6 (Id x) y
+noneI :: AllOfI' ts '[]
+noneI = None
+projI :: In as a => AllOfI as -> a
+projI = unId . proj
+
+newtype Func b a = Func {unFunc :: a -> b}
+type AllOfF as t = AllOfF' as as t
+type AllOfF' ts as t = AllOf' ts as (Func t)
+andF :: (a -> t) -> AllOfF' ts as t -> AllOfF' ts (Type a ': as) t
+andF x y = And (Func x) y
+andF1 :: (forall b. Modify (In ts) p b => a b -> t) -> AllOfF' ts as t -> AllOfF' ts (a <| p ': as) t
+andF1 x y = And1 (Func x) y
+andF2 :: (forall b c. Modify2 (In ts) p b c => a b c -> t) -> AllOfF' ts as t -> AllOfF' ts (a <| p ': as) t
+andF2 x y = And2 (Func x) y
+andF3 :: (forall b c d. Modify3 (In ts) p b c d => a b c d -> t) -> AllOfF' ts as t -> AllOfF' ts (a <| p ': as) t
+andF3 x y = And3 (Func x) y
+andF4 :: (forall b c d e. Modify4 (In ts) p b c d e => a b c d e -> t) -> AllOfF' ts as t -> AllOfF' ts (a <| p ': as) t
+andF4 x y = And4 (Func x) y
+andF5 :: (forall b c d e f. Modify5 (In ts) p b c d e f => a b c d e f -> t) -> AllOfF' ts as t -> AllOfF' ts (a <| p ': as) t
+andF5 x y = And5 (Func x) y
+andF6 :: (forall b c d e f g. Modify6 (In ts) p b c d e f g => a b c d e f g -> t) -> AllOfF' ts as t -> AllOfF' ts (a <| p ': as) t
+andF6 x y = And6 (Func x) y
+noneF :: AllOfF' ts '[] t
+noneF = None
+projF :: In as a => AllOfF as t -> (a -> t)
+projF = unFunc . proj
+
+infixr 0 `andI`, `andI1`, `andI2`, `andI3`, `andI4`, `andI5`, `andI6`, `andF`, `andF1`, `andF2`, `andF3`, `andF4`, `andF5`, `andF6`