Help with defining types

[Yves Cloutier]

Hi,

I'm reading "Domain Modeling Made Functional" by Scott Walschin.

I find it to be a fresh look on how functional languages are well-suited to model business domains. Of course, it using F# (which is very similar to OCaml), it relies very heavily on types to model a domain as well as business processes and workflows.

I'm trying to see how see how the ideas can be converted using Pure. But right off the bat I'm getting stuck on th simplest of tasks - modeling types.

As a simple example, in F#:

type FruitSalad = {
   Apples: AppleType
   Bananas: BananaType
   Cherries: CherryType
}

This is the F# version of a record.

And:

type AppleType =
| GoldenDelicious
| Fuji
| GrannySmith

From the Pure manual I understand the "or" type are written as:

type AppleType GoldenDelicious | AppleType Fuji | AppleType GrannySmith;

But I'm having trouble understanding how to define a type for a record, as in the FruitSalad example.

Any pointers would be helpful.

Regards

[Kurt Pagani]

Hi Yves

I'm not an expert here - Albert will correct my statements if necessary.

My understanding is that "type tags" in Pure (see
https://puredocs.bitbucket.io/pure.html#type-tags) are for
structuring/partitioning the universe of terms in the first place. The notion of
"types" usually used in type theory, programming languages or theorem provers is
far more specialized than in Pure. Of course, you can implement such a type
system in the Pure language itself (e.g. dependent types), but then you have to
write an inference mechanism etc.

Pure provides the "typep" predicate to check whether a term "t" has a type tag "T":

> typep T t

For instance, the type

> type anything _ ;

is the universe of all terms. Actually

> typep anything (f g h 7 +);
1

is always true. You may choose another name for "anything", of course.

Suppose (as an example) you want to define a type "bae" (basic algebraic
expression):

type integer n = intp n || bigintp n; // integer is "int" or "bigint"

type bae u::integer
| bae u::rational
| bae u::symbol
| bae (u::bae * v::bae)
| bae (u::bae + v::bae)
| bae (u::bae - v::bae)
| bae (u::bae / v::bae)
| bae (-u::bae)
| bae (u::bae ^ v::bae)
;

> typep bae (a*b);
1
> typep bae (x+(2*b));
1
> typep bae (sin x);
0

The term "(sin x)" is not a "bae", because it is not defined in the "type tag"
definition of "bae". To cut a long story short, think of predicates which
distinguish certain terms in Pure (purely syntactically). Indeed, you can define
the predicate "baep" (rule):

> baep x = typep bae x;
> baep 8;
1
> baep (u^4);
1
> baep (-qwertz);
1
> baep 3.4444; // float is not a "bae"
0

Maybe the following links will show the subtle differences:

https://en.wikipedia.org/wiki/Herbrand_structure
https://en.wikipedia.org/wiki/Herbrand_interpretation
https://en.wikipedia.org/wiki/Type_theory
https://en.wikipedia.org/wiki/Rewriting


If you are used to Haskell, F#, ML or Coq and so on, then you will recognize
that Pure is a real TRS (especially if you don't load the prelude: pure -n)
which requires a change of thinking: more syntactically than semantically,
though this is my opinion only. I guess this makes Pure so outstanding because
you can "rewrite" almost anything ;-)

--
Kurt

> --
> You received this message because you are subscribed to the Google Groups
> "pure-lang" group.
> To unsubscribe from this group and stop receiving emails from it, send an email
> to pure-lang+...@googlegroups.com
> <mailto:pure-lang+...@googlegroups.com>.
> To post to this group, send email to pure...@googlegroups.com
> <mailto:pure...@googlegroups.com>.
> Visit this group at https://groups.google.com/group/pure-lang.
> For more options, visit https://groups.google.com/d/optout.

[Albert Graef]

Well, you wouldn’t really use a lot of these static data types in a dynamically-typed language, but they might occasionally be useful, so here goes.

First, you’d need to declare the symbolic fruit names, so that they’re not mistaken as variables in the type declaration. Let’s say:

nonfix GoldenDelicious Fuji GrannySmith Chiquita Piemont;
type AppleType GoldenDelicious | AppleType Fuji | AppleType GrannySmith;
type BananaType Chiquita;
type CherryType Piemont;

Second, an idiomatic representation of the FruitSalad record type would simply use a constructor symbol with arguments:

type FruitSalad (FruitSalad _::AppleType _::BananaType _::CherryType);

But then you have to specify the arguments in the right order:

> typep FruitSalad (FruitSalad Fuji Chiquita Piemont);
1
> typep FruitSalad (FruitSalad Fuji Piemont Chiquita);
0

You can use Pure’s record type instead, but you’ll have to go to some lengths to define the type and make it work exactly like the F# type:

type FruitSalad x = recordp x && all (member x) [Apples, Bananas, Cherries] &&
  #keys x == 3 && typep AppleType (x!Apples) && typep BananaType (x!Bananas) &&
  typep CherryType (x!Cherries);

(Yes, that’s tedious and error-prone. However, one could write a little convenience function that would take care of all the mindless drudgery, like enum does for enumeration types.)

That will allow you to specify the different fields in any order:

> typep FruitSalad {Apples=>Fuji, Bananas=>Chiquita, Cherries=>Piemont};
1
> typep FruitSalad {Apples=>Fuji, Cherries=>Piemont, Bananas=>Chiquita};
1

Writing an entire Pure program in that style won’t be much fun, though. If you need these rigid types, you’re much better off writing your program in F#. If you need to check your data for validity, a corresponding predicate would work just fine in Pure. Basically, that’s what Pure’s types are, anyway.

Pure’s types are not really a data structuring device (who needs all that fluff if you can just write down any kind of structured data as a term?), but a means to do data abstraction. The basics of that are sketched out in the Type Tags section of the Pure manual (see the definition of the point type there). The Type Rules section has another example on Peano arithmetic.

Albert

​

--

You received this message because you are subscribed to the Google Groups "pure-lang" group.

To unsubscribe from this group and stop receiving emails from it, send an email to pure-lang+unsubscribe@googlegroups.com.
To post to this group, send email to pure...@googlegroups.com.

Visit this group at https://groups.google.com/group/pure-lang.
For more options, visit https://groups.google.com/d/optout.

--

Dr. Albert Gr"af
Computer Music Research Group, JGU Mainz, Germany
Email:  agg...@gmail.com
WWW:    https://plus.google.com/+AlbertGraef

[Yves Cloutier]

Thank you both for taking the time to answer.

Albert says: who needs all that fluff if you can just write down any kind of structured data as a term?

I have to admit I've always used languages that were statically typed, or for which the paradigm was to model data using data structures, and so it's quite difficult to imagine how work without them!

I guess this is why I was looking for some material to see compare how the same problem is solved, both with types and as terms. Going from OO to Functional was a revelation. And I feel it's going to be the same with term rewriting...once I really get it!

[Albert Graef]

Yeah, it's quite natural when coming from Lisp, but a world that's really alien to ML/Haskell users. ;-) You're not alone. This may help to cheer you up: http://landoflisp.com/

--

You received this message because you are subscribed to the Google Groups "pure-lang" group.
To unsubscribe from this group and stop receiving emails from it, send an email to pure-lang+unsubscribe@googlegroups.com.
To post to this group, send email to pure...@googlegroups.com.
Visit this group at https://groups.google.com/group/pure-lang.
For more options, visit https://groups.google.com/d/optout.

[Albert Graef]

Sorry, I thought there was the "Land of Lisp / Republic of Haskell" strip there, not sure where that went, I can't find it on the Interwebs any more. Now it's a much shorter one.

[Albert Graef]

Ah, it's here: http://www.lisperati.com/landoflisp/panel01.html. You need to click through it. Nerdy humour alert. ;-)