## Stream: Beginner Questions

### Topic: Question about the type

#### Hongjian Jiang (Jul 16 2023 at 09:21):

``````theory Regular_Exp
imports Regular_Set
begin

datatype (atoms: 'a) rexp =
is_Zero: Zero |
is_One: One |
Atom 'a |
Plus "('a rexp)" "('a rexp)" |
Times "('a rexp)" "('a rexp)" |
Star "('a rexp)"

instantiation rexp :: (order) "{order}"
begin
...
end
``````

For the code above, I have several misunderstanding.

1. why atoms in datatype could return a set, in the tutorial the parameter just means the variable.
2. What is the role of first and second order in the class instantiation.

#### Hongjian Jiang (Jul 16 2023 at 12:27):

any helps would be appreciated

#### Mathias Fleury (Jul 16 2023 at 12:35):

I have no clue what you are talking about. In

``````instantiation rexp :: (order) "order"
``````

If you think about applying it to `'a rexp`: The first `(order)` is a constraint about `'a` (in this case, `'a` must be equipped with an order) and the second `order` is the constraint you add to `rexp`. In this case if the case type has an order, then rexp also has an order

#### Hongjian Jiang (Jul 16 2023 at 13:11):

Thank you very much. You mean every rexp here is type order now like Zero is an order, One is an order.

And rexp is a name of order class.

What is the function of is_Zero, is_One and atoms play in the datatype.

#### Mathias Fleury (Jul 16 2023 at 13:14):

No, this is not what I mean…

#### Mathias Fleury (Jul 16 2023 at 13:14):

`Zero` and `One` are elements of a type called `rexp` parametrized by another type

#### Mathias Fleury (Jul 16 2023 at 13:16):

and `is_Zero` and `is_One` are discriminators (see here)

#### Mathias Fleury (Jul 16 2023 at 13:17):

and atoms returns the set of all atoms in the rexp formula

Last updated: Sep 11 2024 at 16:22 UTC