type adviser (Junk)

TypeAdviser.hs

{-# LANGUAGE DataKinds, TypeOperators, KindSignatures, TypeFamilies #-}
{-# LANGUAGE UndecidableInstances, FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE GADTs, MultiParamTypeClasses, FunctionalDependencies #-}

-----------------------------------------------------------------------------
-- |
-- Module : TypeAdviser
-- License : Free
-- 
-- Stability : experimental
-- Portability : non-portable (DataKinds, TypeOperators, KindSignatures,
--               TypeFamilies, UndecidableInstances, FlexibleInstances,
--               FlexibleContexts, GADTs, MultiParamTypeClasses,
--               FunctionalDependencies)
--
-- Description : Helper functions for 'asTypeOf'
--
-- Problem: how to use non-rigid param in data family ??
--
-- > data family T a b
-- > data instance T Int  b = A
-- > data instance T Char b = B
-- > tp0 (A) -- NG
-- > tp0 (A:: T Int Int) -- OK
--
-----------------------------------------------------------------------------
module Data.TypeAdviser where

import GHC.TypeLits
--import Data.Type.Equality
import Data.Typeable


-- | type of n-th argument
--
type family ArgT (a :: *) (idx :: Nat) (len :: Nat) :: * where
    ArgT a 0 0 = a
    ArgT (a -> b) 0 len = a
    ArgT (a -> b) idx len = ArgT b (idx - 1) (len - 1)

-- | type of "return" value
--
type family RetT (a :: *) :: * where
    RetT (a -> b) = RetT b
    RetT a = a


type family NumArg' (a :: *) (offset :: Nat) :: Nat where
    NumArg' (a -> b) offset = NumArg' b (offset + 1)
    NumArg' a offset = offset


-- | num of arguments
--
type family NumArg (a :: *) :: Nat where
    NumArg a = NumArg' a 0


-- | n-th type parameter (form 1 to 5)
--
-- this work for only '* kind type.
type family GetTP (a :: *) (idx :: Nat) :: * where
    GetTP (f a b c d e) 0 = a
    GetTP (f a b c d)   0 = a
    GetTP (f a b c)     0 = a
    GetTP (f a b)       0 = a
    GetTP (f a)         0 = a
    GetTP (f a b c d e) 1 = b
    GetTP (f a b c d)   1 = b
    GetTP (f a b c)     1 = b
    GetTP (f a b)       1 = b
    GetTP (f a b c d e) 2 = c
    GetTP (f a b c d)   2 = c
    GetTP (f a b c)     2 = c
    GetTP (f a b c d e) 3 = d
    GetTP (f a b c d)   3 = d
    GetTP (f a b c d e) 4 = e


-- | replace n-th type parameter (from 1 to 5)
--
-- this work for only * kind type.
type family SetTP (a :: *) (idx :: Nat) (x :: *) :: * where
    SetTP (f a b c d e) 0 x = (f x b c d e)
    SetTP (f a b c d)   0 x = (f x b c d)
    SetTP (f a b c)     0 x = (f x b c)
    SetTP (f a b)       0 x = (f x b)
    SetTP (f a)         0 x = (f x)
    SetTP (f a b c d e) 1 x = (f a x c d e)
    SetTP (f a b c d)   1 x = (f a x c d)
    SetTP (f a b c)     1 x = (f a x c)
    SetTP (f a b)       1 x = (f a x)
    SetTP (f a b c d e) 2 x = (f a b x d e)
    SetTP (f a b c d)   2 x = (f a b x d)
    SetTP (f a b c)     2 x = (f a b x)
    SetTP (f a b c d e) 3 x = (f a b c x e)
    SetTP (f a b c d)   3 x = (f a b c x)
    SetTP (f a b c d e) 4 x = (f a b c d x)

-- | bottom as first argument type
--
-- >>> typeName $ argT0 (undefined :: Int -> Bool -> Char -> Double -> Float)
-- "Int"
argT0 :: a -> ArgT a 0 (NumArg a)
argT0 = undefined

-- | bottom as second argument type
--
-- >>> typeName $ argT1 (undefined :: Int -> Bool -> Char -> Double -> Float)
-- "Bool"
argT1 :: a -> ArgT a 1 (NumArg a)
argT1 = undefined

-- | bottom as third argument type
--
-- >>> typeName $ argT2 (undefined :: Int -> Bool -> Char -> Double -> Float)
-- "Char"
argT2 :: a -> ArgT a 2 (NumArg a)
argT2 = undefined

-- | bottom as 4th argument type
--
-- >>> typeName $ argT3 (undefined :: Int -> Bool -> Char -> Double -> Float)
-- "Double"
argT3 :: a -> ArgT a 3 (NumArg a)
argT3 = undefined

-- | bottom as N-th argument type
--
-- >>> typeName $ argT (Proxy :: Proxy 0) (undefined :: Int -> Bool -> Char -> Double -> Float)
-- "Int"
argT :: Proxy (idx :: Nat) -> a ->  ArgT a idx (NumArg a)
argT = undefined


-- | bottom as "return" value type
--
-- >>> typeName $ retT  (undefined :: Int -> Bool -> Char -> Double -> Float)
-- "Float"
retT :: a -> RetT a
retT = undefined

-- | bottom as first type parameter
--
-- >>> data F a b c d = F
-- >>> typeName $ tp0 (undefined :: F Int Bool Char Double) 
-- "Int"
-- >>> typeName $ tp0 ([1] :: [Int])
-- "Int"
tp0 :: a -> GetTP a 0
tp0 = undefined

-- | bottom as second type parameter
--
-- >>> data F a b c d = F
-- >>> let x = (undefined :: F Int Bool Char Double)
-- >>> typeName $ tp1  (undefined :: F Int Bool Char Double) 
-- "Bool"
tp1 :: a -> GetTP a 1
tp1 = undefined

-- | bottom as third type parameter
--
-- >>> data F a b c d = F
-- >>> typeName $ tp2  (undefined :: F Int Bool Char Double) 
-- "Char"
tp2 :: a -> GetTP a 2
tp2 = undefined

-- | bottom as 4th type parameter
--
-- >>> data F a b c d = F deriving (Typeable)
-- >>> typeName $ tp3  (undefined :: F Int Bool Char Double) 
-- "Double"
tp3 :: a -> GetTP a 3
tp3 = undefined



-- for non-rigid param in data family.
tp0_1 :: f a -> a
tp0_1 = undefined

tp0_2 :: f a b -> a
tp0_2 = undefined

tp1_2 :: f a b -> b
tp1_2 = undefined

tp0_3 :: f a b c -> a
tp0_3 = undefined

tp1_3 :: f a b c -> b
tp1_3 = undefined

tp2_3 :: f a b c -> c
tp2_3 = undefined

tp0_4 :: f a b c d -> a
tp0_4 = undefined

tp1_4 :: f a b c d -> b
tp1_4 = undefined

tp2_4 :: f a b c d -> c
tp2_4 = undefined

tp3_4 :: f a b c d -> d
tp3_4 = undefined


-- | get type signature
--
-- >>> typeName "xxx"
-- "[Char]"
typeName :: (Typeable a) => a -> String
typeName = show . typeRep . (Proxy `as` tp0_1)
--typeName = show . typeRep . (Proxy `as` (tp0))


-- | extented asTypeOf
--
-- >>> data F a b = F deriving (Typeable)
-- >>> typeName $ (undefined :: Int -> F a Bool -> Float) `as` (tp0 . argT1) $ (undefined :: String)
-- "Int -> F [Char] Bool -> Float"
as :: a -> (a->b) -> b -> a
as x f y = const x (asTypeOf (f x) y)




-- | bottom as first type parameter replaaced type
--
-- >>> data F a b c d = F deriving (Typeable)
-- >>> typeName $ settp0 (undefined :: F Int Bool Char Double) "x"
-- "F [Char] Bool Char Double"
settp0 :: a -> b -> SetTP a 0 b
settp0 = undefined

-- | bottom as second type parameter replaaced type
--
-- >>> data F a b c d = F deriving (Typeable)
-- >>> typeName $ settp1  (undefined :: F Int Bool Char Double) "x"
--"F Int [Char] Char Double"
settp1 :: a -> b -> SetTP a 1 b
settp1 = undefined

-- | bottom as third type parameter replaaced type
--
-- >>> data F a b c d = F deriving (Typeable)
-- >>> typeName $ settp2  (undefined :: F Int Bool Char Double) "x"
--"F Int Bool [Char] Double"
settp2 :: a -> b -> SetTP a 2 b
settp2 = undefined

-- | bottom as 4th type parameter replaaced type
--
-- >>> data F a b c d = F deriving (Typeable)
-- >>> typeName $ settp3  (undefined :: F Int Bool Char Double) "x"
--"F Int Bool Char [Char]"
settp3 :: a -> b -> SetTP a 3 b
settp3 = undefined



settp0_1 :: f a -> x -> f x
settp0_1 = undefined

settp0_2 :: f a b -> x -> f x b
settp0_2 = undefined

settp1_2 :: f a b -> x -> f a x
settp1_2 = undefined

settp0_3 :: f a b c -> x -> f x b c
settp0_3 = undefined

settp1_3 :: f a b c -> x -> f a x c
settp1_3 = undefined

settp2_3 :: f a b c -> x -> f a b x
settp2_3 = undefined

settp0_4 :: f a b c d -> x -> f x b c d
settp0_4 = undefined

settp1_4 :: f a b c d -> x -> f a x c d
settp1_4 = undefined

settp2_4 :: f a b c d -> x -> f a b x d
settp2_4 = undefined

settp3_4 :: f a b c d -> x -> f a b c x
settp3_4 = undefined