Re: [GHC] #12708: RFC: Representation polymorphic Num

16 Oct 2016

      #12708: RFC: Representation polymorphic Num
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Core Libraries    |              Version:  8.0.1
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by Iceland_jack):

 If we did like [https://github.com/mikeizbicki/subhask subhask] we could
 even interpret `==` in a different logic

 {{{#!hs
 -- This doesn't work unless it's closed
 type family
   Rep (rep :: RuntimeRep) :: RuntimeRep where
   Rep IntRep         = IntRep
   Rep DoubleRep      = IntRep
   Rep PtrRepUnlifted = IntRep
   Rep PtrRepLifted   = PtrRepLifted
   -- etc.

 class Eq (a :: TYPE rep) where
   type Logic (a :: TYPE rep) :: TYPE (Rep rep)
   (==) :: a -> a -> Logic a

 instance Eq (Int :: Type) where
   type Logic Int = Bool
   (==) :: Int -> Int -> Bool
   (f == g) a = f a == g a

 instance Eq (Int# :: TYPE IntRep) where
   type Logic Int# = Int#
   (==) :: Int# -> Int# -> Int#
   (==) = (==#)

 instance Eq (Double# :: TYPE DoubleRep) where
   type Logic Double# = Int#
   (==) :: Double# -> Double# -> Int#
   (==) = (==##)
 }}}

 Come on, you know you want it ;) we can use the same `==` for EDSLs?

 {{{#!hs
 data Exp :: Type -> Type where
   Eq :: a -> a -> Exp Bool

 instance Eq (Exp a) where
   type Logic (Exp a) = Exp Bool
   (==) :: Exp a -> Exp a -> Exp Bool
   (==) = Eq
 }}}

 or

 {{{#!hs
 data TY = INT | BOOL

 data Exp :: TY -> Type where
   EqI :: INT  -> INT  -> Exp BOOL
   EqB :: BOOL -> BOOL -> Exp BOOL

 instance Eq (Exp INT) where
   type Logic (Exp INT) = Exp BOOL
   (==) :: Exp INT -> Exp INT -> Exp BOOL
   (==) = EqI

 instance Eq (Exp BOOL) where
   type Logic (Exp BOOL) = Exp BOOL
   (==) :: Exp BOOL -> Exp BOOL -> Exp BOOL
   (==) = EqB
 }}}

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12708#comment:13
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler