[Haskell-cafe] type-level integers, type-level operators, and most specific overlapping instance
TP
paratribulations at free.fr
Sat Sep 21 18:29:08 CEST 2013
adam vogt wrote:
> 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
Thanks a lot Adam. It is a pity I did not think to this solution myself.
Below is the full code for a working version (however still using a more
general definition of multiplication compared to yours).
But I have still a question: is the behavior of GHC correct in the example
of my initial post? It is OK it does not look at the most specific instance
by examining the instance context? Is it OK, or is it a deficiency?
Thanks,
TP
---------------------------------
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverlappingInstances #-}
import Prelude hiding ((*))
data Nat = Zero | Succ Nat
deriving ( Show, Eq, Ord )
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 Scalar Scalar where
s * s' = Mult s s'
instance Multiplication Scalar (Tensor n) (Tensor n) where
s * t = Mult s t
instance Multiplication (Tensor n) Scalar (Tensor n) where
t * s = Mult s t
main = do
let s = Tensor :: Scalar
let a = s*s
print a
More information about the Haskell-Cafe
mailing list