[Haskell-cafe] Type trickery
The well-known ST monad uses an ingenious hack to make it impossible for distinct ST computations to interact with each other. Is there a way to do something similar so that I can create cursors that reference a (mutable) container, and then write a function that takes two cursor arguments which are statically guaranteed to refer to the same container? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type trickery
On 16 March 2011 11:31, Andrew Coppin andrewcop...@btinternet.com wrote: The well-known ST monad uses an ingenious hack to make it impossible for distinct ST computations to interact with each other. Is there a way to do something similar so that I can create cursors that reference a (mutable) container, and then write a function that takes two cursor arguments which are statically guaranteed to refer to the same container? You could define a function: withContainer ∷ (∀ s. Container s → α) → α which creates a container, parameterizes it with an 's' that is only scoped over the continuation and applies the continuation to the created container. If you then define a function to create a cursor from it like: cursor ∷ Container s → Cursor s it is statically guaranteed that two Cursors parameterized with the same 's' refer to the same container: foo ∷ Cursor s → Cursor s → ... because the only way to create a Container s is through withContainer. Regards, Bas ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type trickery
You could define a function: withContainer ∷ (∀ s. Container s → α) → α which creates a container, parameterizes it with an 's' that is only scoped over the continuation and applies the continuation to the created container. Hmm, yes. That will work, but I wonder if there's some way of doing this that doesn't limit the scope of the container to one single span of code... ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type trickery
I fail to see how does it limit the scope. 16.03.2011 15:05, Andrew Coppin пишет: You could define a function: withContainer ∷ (∀ s. Container s → α) → α which creates a container, parameterizes it with an 's' that is only scoped over the continuation and applies the continuation to the created container. Hmm, yes. That will work, but I wonder if there's some way of doing this that doesn't limit the scope of the container to one single span of code... ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type trickery
Hi Andrew, Andrew Coppin wrote: You could define a function: withContainer ∷ (∀ s. Container s → α) → α which creates a container, parameterizes it with an 's' that is only scoped over the continuation and applies the continuation to the created container. Hmm, yes. That will work, but I wonder if there's some way of doing this that doesn't limit the scope of the container to one single span of code... You can write helper functions which take containers as argument by parameterizing these helper functions over s: takesTwoContainers :: Container s1 - Container s2 - ... takesTwoContainers c1 c2 = ... -- c1 and c2 can be used here This function could be called like this: withContainer (\c1 - withContainer (\c2 - takesTwoContainers c1 c2)) -- c1 and c2 can be used here In this example, the scope of the containers is not limited to a single span of code. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type trickery
Hmm, yes. That will work, but I wonder if there's some way of doing this that doesn't limit the scope of the container to one single span of code... You can write helper functions which take containers as argument by parameterizing these helper functions over s: takesTwoContainers :: Container s1 - Container s2 - ... takesTwoContainers c1 c2 = ... -- c1 and c2 can be used here This function could be called like this: withContainer (\c1 - withContainer (\c2 - takesTwoContainers c1 c2)) -- c1 and c2 can be used here In this example, the scope of the containers is not limited to a single span of code. What you can't do is write functions such as foo :: Container x - (Cursor x, Cursor x) for example. Perhaps this property is just too tricky to check in the type system. It's quite possible to check it at run-time; I'd just prefer to check at compile-time, if it's not too difficult to implement. I thought of a further complication: What happens if you concatinate two containers? Then cursors to each of the original containers all become valid for the new, concatenated container. I suppose you could issue a new phantom type variable for the concatenated version, but the whole idea of mutable containers is to, you know, mutate them. Given the above, perhaps it's just not possible to check this kind of thing statically at all. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type trickery
On Wed, Mar 16, 2011 at 12:05:56PM +, Andrew Coppin wrote: withContainer ∷ (∀ s. Container s → α) → α Hmm, yes. That will work, but I wonder if there's some way of doing this that doesn't limit the scope of the container to one single span of code... You can just pack the container into an existential and pass that around freely. Only the use of cursors is limited into a scope where the owning container's type variable is visible (which you get by unpacking the existential). Lauri ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type trickery
On Wed, Mar 16, 2011 at 7:52 AM, Andrew Coppin andrewcop...@btinternet.com wrote: Hmm, yes. That will work, but I wonder if there's some way of doing this that doesn't limit the scope of the container to one single span of code... You can write helper functions which take containers as argument by parameterizing these helper functions over s: takesTwoContainers :: Container s1 - Container s2 - ... takesTwoContainers c1 c2 = ... -- c1 and c2 can be used here This function could be called like this: withContainer (\c1 - withContainer (\c2 - takesTwoContainers c1 c2)) -- c1 and c2 can be used here In this example, the scope of the containers is not limited to a single span of code. What you can't do is write functions such as foo :: Container x - (Cursor x, Cursor x) for example. I don't follow. foo = cursor cursor Did you mean to have some extra condition on foo that can't be satisfied? Luke ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type trickery
On 3/16/11 9:52 AM, Andrew Coppin wrote: Hmm, yes. That will work, but I wonder if there's some way of doing this that doesn't limit the scope of the container to one single span of code... You can write helper functions which take containers as argument by parameterizing these helper functions over s: takesTwoContainers :: Container s1 - Container s2 - ... takesTwoContainers c1 c2 = ... -- c1 and c2 can be used here This function could be called like this: withContainer (\c1 - withContainer (\c2 - takesTwoContainers c1 c2)) -- c1 and c2 can be used here In this example, the scope of the containers is not limited to a single span of code. What you can't do is write functions such as foo :: Container x - (Cursor x, Cursor x) for example. -- ? foo cx = (curse cx, curse cx) Perhaps this property is just too tricky to check in the type system. It's quite possible to check it at run-time; I'd just prefer to check at compile-time, if it's not too difficult to implement. It sounds like you want something based on memory regions. The ST monad uses a restricted version of regions, but there are more general versions which allow for comparing region names for equality etc (as opposed to ST where the existential quantification requires the types to unify or be unequal). Try googling around. -- Live well, ~wren ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] type trickery
Hello haskell-cafe! After making data Number = Zero | Succ Number an instance of Integral, I wondered how I could do the same with galois fields. So starting with Z mod p, I figured I'd need something like this data GF = GF Integer Integer so that each element of the finite field would remember p. However I can't think of a way to use the typesystem to ensure that p is always the same. I think that would need an infinite number of different types, but the type hackers here probably know something better. Adrian PGP.sig Description: Signierter Teil der Nachricht ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type trickery
On Dec 20, 2007 9:34 AM, Adrian Neumann [EMAIL PROTECTED] wrote: Hello haskell-cafe! After making data Number = Zero | Succ Number an instance of Integral, I wondered how I could do the same with galois fields. So starting with Z mod p, I figured I'd need something like this data GF = GF Integer Integer so that each element of the finite field would remember p. However I can't think of a way to use the typesystem to ensure that p is always the same. I think that would need an infinite number of different types, but the type hackers here probably know something better. Yes, you can have some fun by taking your Number definition to the type level: data Zero-- phantom type, no implementation data Succ a -- same class Runtimify a where runtimify :: a - Integer instance Runtimify Zero where runtimify _ = 0 instance (Runtimify a) = Runtimify (Succ a) where runtimify _ = 1 + runtimify (undefined :: a) data GF p = GF Integer instance (Runtimify p) = Num (GF p) where -- you fill in the rest :-) Note that p is encoded in only a type variable, so you'll have to use runtimify (sorry for the silly name) to get it out. Luke ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
