## Stream: Beginner Questions

### Topic: Defining a function between function types

#### P Paturi (Apr 03 2023 at 11:57):

Hello everyone! I'm trying to define a function between function types and I'm not sure what the correct syntax is. Generally, I want to map function f to function g such that the definition of g depends on f.
More specifically, I have a configuration c which is a function from a monoid (int for the sake of simplicity) to a finite alphabet, and want to define a shift map which maps it to another configuration e such that e(x) = c(x+r) where r is some shift constant.
I have defined the type synonym 'a config = "'a => alfa" (where alfa is the alphabet) and I am trying to define the shift as a function 'a config => => 'a => 'a config (where the second argument would be the shift constant).

#### Kevin Kappelmann (Apr 04 2023 at 06:34):

I am a bit lost what you want to do precisely. How would you define in mathematically? You can use Latex on Zulip
https://zulip.com/help/format-your-message-using-markdown#latex

#### P Paturi (Apr 04 2023 at 11:36):

I have a finite alphabet $A$ and the space of configurations $A^Z$, which are just functions $c:Z \rightarrow A$ (I am aware this could be done with bi-infinite lists, but I want to be able to generalize $Z$ to an arbitrary monoid later.) Let $r \in Z$. A shift map $\sigma_r: A^Z \rightarrow A^Z$ maps $c$ such that $\sigma_r (c) (x) = c (x+r)$, which is what I'm trying to define.

#### Manuel Eberl (Apr 04 2023 at 13:06):

definition shift :: "int ⇒ (int ⇒ 'a) ⇒ int ⇒ 'a" where
"shift r c x = c (x + r)"


Or, equivalently, this:

definition shift :: "int ⇒ (int ⇒ 'a) ⇒ int ⇒ 'a" where
"shift r c = c ∘ ((+) r)"


#### P Paturi (Apr 20 2023 at 07:48):

This would not work for what I want, because what I want out is a function of type int => 'a, not just 'a. This is so I can for example create sets of shifted configurations. (If anyone has an alternative way of defining configurations on int in mind, that could also work)

#### Simon Roßkopf (Apr 20 2023 at 08:26):

The types int ⇒ (int ⇒ 'a) ⇒ int ⇒ 'a and int ⇒ (int ⇒ 'a) ⇒ (int ⇒ 'a) are equal. So partially applying, like shift r c should give you what you need

#### P Paturi (Apr 20 2023 at 08:41):

Ah, I see. Thank you!

Last updated: Dec 07 2023 at 08:19 UTC