type-level integers, type-level operators, and most specific overlapping instance
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
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
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
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
TP wrote:
But I have still a question: is the behavior of GHC correct in the example of my initial post?
See here: http://www.haskell.org/ghc/docs/7.6.3/html/users_guide/type-class-extensions... """ When matching, GHC takes no account of the context of the instance declaration (context1 etc). GHC's default behaviour is that exactly one instance must match the constraint it is trying to resolve. """ My misunderstanding came from a confusion between a "context" and a "constraint". The context is what is before the =>, and the constraint is what is after, i.e. the main part of the instance declaration. This is the reason why my context using an inequality test on type-level integers was not taken into account: if I understand well there must be only one instance that matches the constraint, independently from the contexts, before GHC checks that the instance context is indeed respected. The OverlappingInstances option only helps to have only one matching instance (independently from the contexts): if several instances match, but there is a more specific one, GHC selects this one and then checks the corresponding instance context. Thanks, TP
On Sun, Sep 22, 2013 at 11:07 AM, TP
My misunderstanding came from a confusion between a "context" and a "constraint". The context is what is before the =>, and the constraint is what is after, i.e. the main part of the instance declaration.
Hi TP, I think context and constraint mean the same thing. The haskell report uses the word context for http://www.haskell.org/onlinereport/decls.html for the whole list and constraint for one part of that list (Eq a). With the extension -XConstraintKinds both of those are called Constraint. In other words:
instance Context => InstanceHead
instance (Constraint, Constraint2) => InstanceHead
Regards, Adam
adam vogt wrote:
I think context and constraint mean the same thing. The haskell report uses the word context for http://www.haskell.org/onlinereport/decls.html for the whole list and constraint for one part of that list (Eq a). With the extension -XConstraintKinds both of those are called Constraint. In other words:
instance Context => InstanceHead
instance (Constraint, Constraint2) => InstanceHead
This is indeed more in accordance with what I believe to be a context or a constraint. But, it seems that in this page http://www.haskell.org/ghc/docs/7.6.3/html/users_guide/type-class-extensions... the vocabulary is different: """ instance context1 => C Int a where ... -- (A) instance context2 => C a Bool where ... -- (B) instance context3 => C Int [a] where ... -- (C) instance context4 => C Int [Int] where ... -- (D) The instances (A) and (B) match the constraint C Int Bool, but (C) and (D) do not. When matching, GHC takes no account of the context of the instance declaration (context1 etc). [...] The -XOverlappingInstances flag instructs GHC to allow more than one instance to match, provided there is a most specific one. For example, the constraint C Int [Int] matches instances (A), (C) and (D), but the last is more specific, and hence is chosen. If there is no most-specific match, the program is rejected. """ So, what do I miss? Isn't the vocabulary different here? And I do not understand what is written if I take your definition (which is indeed the definition in the Haskell report). Thanks in advance, TP
participants (2)
-
adam vogt -
TP