Is it possible to get values out of a datatype?

```
theory DataTypeLHS
imports Main begin
datatype ('a, 'b) myType = MyType 'a 'b
primrec getValues :: "('a, 'b) myType ⇒ ('a*'b)"
where
"getValues mt = (let (MyType a b) = mt in (a,b)"
```

(this does not parse with any of the function definition mechanisms)

or this is completely against the design of datatypes, concerning abstraction?

My use case is to have a type for something, but I need to access its constituents for later processing. Again, is `type_synonym`

my tool?

either selectors or with case

```
datatype ('a, 'b) myType = MyType (myfst: 'a) (mysnd: 'b)
primrec getValues :: "('a, 'b) myType ⇒ ('a*'b)"
where
"getValues mt = (myfst mt, mysnd mt)"
```

or

```
primrec getValues :: "('a, 'b) myType ⇒ ('a*'b)"
where
"getValues mt = (case mt of MyType (a,b) => (a b))"
```

I see. I tried `let`

and it did not work.

Gergely Buday said:

(this does not parse with any of the function definition mechanisms)

Your problem has nothing to do with function definition mechanisms but rather with `let`

. Note that `let`

, like `λ`

, works only with certain patterns, for example `(_, _)`

. The constructors used in these patterns seem to be introduced using a different, more low-level mechanism.

Thank you @Mathias Fleury , the `case`

construction solved my problem.

For a naive solution, I did `aValueFormMyType`

and `bValueFromMyType`

functions to get the values but of course there is a simple and elegant solution for that.

You can also use the `fun`

construct with the function argument being a pattern, something like this:

```
fun getValues :: "('a, 'b) myType ⇒ ('a × 'b)" where
"getValues (MyType a b) = (a, b)"
```

Last updated: Feb 27 2024 at 08:17 UTC