Stream: Beginner Questions

Topic: Instantiation with multiple type params

Matthew Torrence (Nov 17 2022 at 13:26):

I have a really simple example that I can't get working, involving instantiatations with multiple type parameters:

datatype ('a, 'b) MyT = MyT 'b

instantiation MyT :: (_, plus) plus
begin
fun plus_MyT :: "('l, 'a::plus) MyT ⇒ ('l, 'a) MyT ⇒ ('l, 'a) MyT" where
  "plus_MyT (MyT a) (MyT b) = MyT (a + b)"
instance ..
end

When I run this, I get an error on the constraint 'a::plus saying

Sort constraint plus inconsistent with default type for type variable "'a"⌂

So it looks like for the second type param, it's reading the constraint for the first param _? Curiously, when I write

instantiation MyT :: (plus, _) plus

it _does_ compile, but note that this is obviously not what I want to do, because then I don't get an instance for, say, (unit, nat) MyT:

value "MyT 5 + (MyT 6 :: (unit, nat) MyT)"

gives error:

Type unification failed: No type arity unit :: plus

I really don't understand why this second example is valid but the first one isn't

Mathias Fleury (Nov 17 2022 at 13:29):

datatype ('a, 'b) MyT = MyT 'b

instantiation MyT :: (_, plus) plus
begin
fun plus_MyT :: "('a, 'b::plus) MyT ⇒ ('a, 'b) MyT ⇒ ('a, 'b) MyT" where
  "plus_MyT (MyT a) (MyT b) = MyT (a + b)"
instance ..
end

Mathias Fleury (Nov 17 2022 at 13:30):

the type unification gives the names 'a, 'b, and so on. So your 'l, 'a::plus does not work

Matthew Torrence (Nov 17 2022 at 13:30):

gotcha. Huh. Interesting. Very quick response though appreciated

Matthew Torrence (Nov 17 2022 at 13:34):

to be fair to my original example, of which this is an MWE, my actual type has something like

datatype ('l, 'a) MyT = MyT 'a

which is why I still had the 'l and 'a naming going on

Last updated: Apr 26 2024 at 20:16 UTC