Gergely Buday (Aug 03 2023 at 13:04): Gergely Buday (Aug 03 2023 at 13:04):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?
Mathias Fleury (Aug 03 2023 at 13:05):either selectors or with case
Mathias Fleury (Aug 03 2023 at 13:07):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.
Wolfgang Jeltsch (Aug 03 2023 at 13:11):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.
Gergely Buday (Aug 03 2023 at 13:14):Thank you @Mathias Fleury , the case construction solved my problem.
Gergely Buday (Aug 03 2023 at 13:16):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.
Wolfgang Jeltsch (Aug 03 2023 at 13:40):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: Nov 13 2025 at 04:27 UTC