[Haskell-cafe] type-level integers, type-level operators, and most specific overlapping instance
adam vogt
vogt.adam at gmail.com
Sat Sep 21 17:07:46 CEST 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 <paratribulations at free.fr> 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
More information about the Haskell-Cafe
mailing list