Stream: Beginner Questions

Topic: Getting values out of a datatype


view this post on Zulip 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?

view this post on Zulip Mathias Fleury (Aug 03 2023 at 13:05):

either selectors or with case

view this post on Zulip 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))"

view this post on Zulip Gergely Buday (Aug 03 2023 at 13:10):

I see. I tried let and it did not work.

view this post on Zulip 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.

view this post on Zulip Gergely Buday (Aug 03 2023 at 13:14):

Thank you @Mathias Fleury , the case construction solved my problem.

view this post on Zulip 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.

view this post on Zulip 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: Feb 27 2024 at 08:17 UTC