Re: [Haskell-cafe] type-level integers, type-level operators, and most specific overlapping instance

21 Sep 2013

      Hi TP,

You can add another instance to cover the case that everything is zero.
Then you don't need the :<. Also it's convenient to arrange for the
a,b,c to be the argument to Tensor, as given below:

class Multiplication a b c | a b -> c where
    (*) :: Tensor a -> Tensor b -> Tensor c

instance Multiplication Zero Zero Zero where
        s * t = Mult s t
instance Multiplication Zero n n where
        s * t = Mult s t
instance Multiplication n Zero n where
        t * s = Mult s t

Regards,
Adam

On Sat, Sep 21, 2013 at 10:38 AM, TP  wrote:
...
Hi everybody,
I encouter some problem in my code in the following simple example: two
instances overlap for the multiplication sign `*`. The
`OverlappingInstances` extension is of no help because it seems GHC does not
look at the instance context to decide which instance is the most specific.
file:///usr/share/doc/ghc-doc/html/users_guide/type-class-
extensions.html#instance-overlap
How to make GHC realize that in the second instance below, the instance
context is not satisfied, such that the first instance has to be used?
(Indeed, a Scalar is a `Tensor 'Zero`, so the strict inequality `'Zero :< n`
is not satisfied in the context).
--------------------------------------------
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverlappingInstances #-}
import Prelude hiding ((*))
data Nat = Zero | Succ Nat
    deriving ( Show, Eq, Ord )
type family (m::Nat) :< (n::Nat) :: Bool -- Here Bool is a kind.
type instance m :< 'Zero = 'False
type instance 'Zero :< ('Succ n) = 'True
type instance ('Succ m) :< ('Succ n) = m :< n
data Tensor :: Nat -> * where
    Tensor :: Tensor order
    Mult   :: Scalar -> Tensor order -> Tensor order
deriving instance Show (Tensor order)
type Scalar = Tensor 'Zero
class Multiplication a b c | a b -> c where
    (*) :: a -> b -> c
instance Multiplication Scalar (Tensor n) (Tensor n) where
        s * t = Mult s t
instance (('Zero :< n) ~ 'True) =>
             Multiplication (Tensor n) Scalar (Tensor n) where
        t * s = Mult s t
main = do
let s = Tensor :: Scalar
let a = s*s
print a
--------------------------------------------
that yields at compilation:
Overlapping instances for Multiplication
                                Scalar Scalar (Tensor 'Zero)
      arising from a use of `*'
    Matching instances:
      instance [overlap ok] Multiplication Scalar (Tensor n) (Tensor n)
        -- Defined at
test_overlapping_instance_with_typelevelinteger_test.hs:31:10
      instance [overlap ok] ('Zero :< n) ~ 'True =>
                            Multiplication (Tensor n) Scalar (Tensor n)
        -- Defined at
test_overlapping_instance_with_typelevelinteger_test.hs:34:10
    In the expression: s * s
    In an equation for `a': a = s * s
    In the expression:
      do { let s = ...;
           let a = s * s;
           print a }
Thanks in advance,
TP
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type-level integers, type-level operators, and most specific overlapping instance

adam vogt