haskellari / lattices

Fine-grained lattice primitives for Haskell
BSD 3-Clause "New" or "Revised" License
35 stars 15 forks source link

[Question]: How to correctly use the library for the construction of a BoundedLattice #22

Open aleSuglia opened 8 years ago

aleSuglia commented 8 years ago

Hi @phadej,

I'm working with your library in order to define a bounded lattice. I've seen that everything should be constructed using joins and meets methods. I want to construct it from a set or a range of values. Please, can you give me an example?

I've tried to use the methods joins and meets in this way:

      let s = Data.Set.fromList [1,2,3,4,5]
      let a = L.joins s
      let b = L.meets s

I don't understand how to obtain a single bounded lattice using the defined methods. I've also tried to take the bottom and top element from a and b, but I obtain some errors. I think that I'm not correctly using the methods.

Thank you for your help.

Cheers, Alessandro

phadej commented 8 years ago

Sorry, I'm not really understand your question. Do you want to construct bounded ordered lattice of elements 1..5 ? i.e. a to be 1 and b = 5?

aleSuglia commented 8 years ago

I want to create, from the set of integers [1..5], a bounded ordered lattice which should have as top element 5 and as bottom element 1.

phadej commented 8 years ago

You can use Ordered newtype:

> Ordered 1 /\ Ordered 2 :: Ordered Int
Ordered {getOrdered = 1}

If you really need bounded lattice to 1 and 5, you'd need to create a new newtype:

newtype Int1to5 = I Int

instance JoinSemiLattice Int1to5 where
    I a \/ I b = I . getOrdered $ Ordered a \/ Ordered b

instance BoundedJoinSemiLattice Int1to5 where
    bottom = I 1

if you want to create lattices based on runtime sets (i.e. not known at the compile time, so you cannot create a newtype for each), then the situation is quite difficult (AFAIK possible though). I'm not sure if you really want to do that.

aleSuglia commented 8 years ago

I don't know why it's not possible to define a simple concept like a set of natural numbers from 1 to 5, following the natural ordering. In this lattice, the maximum element should be 5 and the minimum 1. Why is so difficult and strange to define it in your library?

Maybe I'm missing the point, sorry about that. I hope that you can provide to me more information because I've not understood how to use your example.

phadej commented 8 years ago

The problem of defining set of natural numbers from 1 to 5 is not a problem with this library. The question is more general: How to define type of natural numbers from 1 to 5? you can do

data Nat1to5 = N1 | N2 | N3 | N4 | N5

and write all required instances (including classes from this library) for it.

if you want a quotient type Int | \n -> 1 <= n && n <= 5, then it's not possible simply in Haskell (or any other mainstream language AFAIK).


I'm not sure what you are trying to do. If you could write what you are trying to do in some other language (preferably statically typed), then I might be able to convert it to Haskell.