Seems that by making a class you can "prove" by requiring this isomorphism:
class (To r ~ v, From v ~ r) -- , To (From v :: Rep a x) ~ v)
=> TypeGeneric a (r :: Rep a x) (v :: a)
where
type To r :: a
type From v :: Rep a x
See attachment or [1] for the whole file.
Cheers, Oleg
[1]: https://gist.github.com/phadej/fab7c627efbca5cba16ba258c8f10337
On 31.08.2017 23:22, David Feuer wrote:
> One other thing I should add. We'd really, really like to have isomorphism
> evidence:
>
> toThenFrom :: pr p -> To (From x :: Rep a p) :~: (x :: a)
> fromThenTo :: pr1 a -> pr2 (r :: Rep a p) -> From (To r :: a) :~: (r :: Rep
> a p)
>
> I believe these would make the To and From families considerably more
> useful. Unfortunately, while I'm pretty sure those are completely legit for
> any Generic-derived types, I don't think there's ever any way to prove
> them in Haskell! Ugh.
>
> On Thursday, August 31, 2017 3:37:15 PM EDT David Feuer wrote:
>> I've been thinking for several weeks that it might be useful to offer
>> type-level generics. That is, along with
>>
>> to :: Rep a k -> a
>> from :: a -> Rep a
>>
>> perhaps we should also derive
>>
>> type family To (r :: Rep a x) :: a
>> type family From (v :: a) :: Rep a x
>>
>> This would allow us to use generic programming at the type level
>> For example, we could write a generic ordering family:
>>
>> class OrdK (k :: Type) where
>> type Compare (x :: k) (y :: k) :: Ordering
>> type Compare (x :: k) (y :: k) = GenComp (Rep k ()) (From x) (From y)
>>
>> instance OrdK Nat where
>> type Compare x y = CmpNat x y
>>
>> instance OrdK Symbol where
>> type Compare x y = CmpSymbol x y
>>
>> instance OrdK [a] -- No implementation needed!
>>
>> type family GenComp k (x :: k) (y :: k) :: Ordering where
>> GenComp (M1 i c f p) ('M1 x) ('M1 y) = GenComp (f p) x y
>> GenComp (K1 i c p) ('K1 x) ('K1 y) = Compare x y
>> GenComp ((x :+: y) p) ('L1 m) ('L1 n) = GenComp (x p) m n
>> GenComp ((x :+: y) p) ('R1 m) ('R1 n) = GenComp (y p) m n
>> GenComp ((x :+: y) p) ('L1 _) ('R1 _) = 'LT
>> GenComp ((x :+: y) p) ('R1 _) ('L1 _) = 'GT
>> GenComp ((x :*: y) p) (x1 ':*: y1) (x2 ':*: y2) =
>> PComp (GenComp (x p) x1 x2) (y p) y1 y2
>> GenComp (U1 p) _ _ = 'EQ
>> GenComp (V1 p) _ _ = 'EQ
>>
>> type family PComp (c :: Ordering) k (x :: k) (y :: k) :: Ordering where
>> PComp 'EQ k x y = GenComp k x y
>> PComp x _ _ _ = x
>>
>> For people who want to play around with the idea, here are the definitions
>> of To and From
>> for lists:
>>
>> To ('M1 ('L1 ('M1 'U1))) = '[]
>> To ('M1 ('R1 ('M1 ('M1 ('K1 x) ':*: 'M1 ('K1 xs))))) = x ': xs
>> From '[] = 'M1 ('L1 ('M1 'U1))
>> From (x ': xs) = 'M1 ('R1 ('M1 ('M1 ('K1 x) ':*: 'M1 ('K1 xs))))
>>
>> David
>
> _______________________________________________
> ghc-devs mailing list
> ghc-devs@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# OPTIONS_GHC -fprint-explicit-kinds #-}
import Data.Kind
import Data.Type.Equality
import GHC.Generics
import GHC.TypeLits
-------------------------------------------------------------------------------
-- Class
-------------------------------------------------------------------------------
class (To r ~ v, From v ~ r) -- , To (From v :: Rep a x) ~ v)
=> TypeGeneric a (r :: Rep a x) (v :: a)
where
type To r :: a
type From v :: Rep a x
-------------------------------------------------------------------------------
-- Iso
-------------------------------------------------------------------------------
toThenFrom
:: forall a x (r :: Rep a x) (v :: a) pr. TypeGeneric a r v
=> pr x
-> To (From v :: Rep a x) :~: (v :: a)
toThenFrom _ = Refl
fromThenTo
:: forall a x (r :: Rep a x) (v :: a) pr1 pr2. TypeGeneric a r v
=> pr1 a -> pr2 (r :: Rep a x)
-> From (To r :: a) :~: (r :: Rep a x)
fromThenTo _ _ = Refl
-------------------------------------------------------------------------------
-- List
-------------------------------------------------------------------------------
instance TypeGeneric [k] ('M1 ('L1 ('M1 'U1))) '[] where
type To ('M1 ('L1 ('M1 'U1))) = '[]
type From '[] = 'M1 ('L1 ('M1 'U1))
instance TypeGeneric [k] ('M1 ('R1 ('M1 ('M1 ('K1 x) ':*: 'M1 ('K1 xs))))) (x ': xs) where
type To ('M1 ('R1 ('M1 ('M1 ('K1 x) ':*: 'M1 ('K1 xs))))) = x ': xs
type From (x ': xs) = 'M1 ('R1 ('M1 ('M1 ('K1 x) ':*: 'M1 ('K1 xs))))
-------------------------------------------------------------------------------
-- OrdK
-------------------------------------------------------------------------------
class OrdK (k :: Type) where
type Compare (x :: k) (y :: k) :: Ordering
type Compare (x :: k) (y :: k) = GenComp (Rep k ()) (From x) (From y)
instance OrdK Nat where
type Compare x y = CmpNat x y
instance OrdK Symbol where
type Compare x y = CmpSymbol x y
instance OrdK [a] -- No implementation needed!
type family GenComp k (x :: k) (y :: k) :: Ordering where
GenComp (M1 i c f p) ('M1 x) ('M1 y) = GenComp (f p) x y
GenComp (K1 i c p) ('K1 x) ('K1 y) = Compare x y
GenComp ((x :+: y) p) ('L1 m) ('L1 n) = GenComp (x p) m n
GenComp ((x :+: y) p) ('R1 m) ('R1 n) = GenComp (y p) m n
GenComp ((x :+: y) p) ('L1 _) ('R1 _) = 'LT
GenComp ((x :+: y) p) ('R1 _) ('L1 _) = 'GT
GenComp ((x :*: y) p) (x1 ':*: y1) (x2 ':*: y2) =
PComp (GenComp (x p) x1 x2) (y p) y1 y2
GenComp (U1 p) _ _ = 'EQ
GenComp (V1 p) _ _ = 'EQ
type family PComp (c :: Ordering) k (x :: k) (y :: k) :: Ordering where
PComp 'EQ k x y = GenComp k x y
PComp x _ _ _ = x
signature.asc
Description: OpenPGP digital signature
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
