{- Disclaimer: I'm rather new to Haskell and completely new to this board.
I may not use the correct terminology in all cases, but I hope my intention becomes clear when you have a look at the code-snippets. -} Hey ho, Is there any way two find out whether two variables refer to the same cell? That is I'm looking for a notion of identity (compareable to == in Java) as opposed to equality (== in Haskell). The motivation is that I need to find out whether two infinite structures are identical. Consider this Haskell implementation of the simple typed lambda calculus (STLC) with the primitive Type "TyUnit" and the primitive value "TmUnit": data Type = TyUnit | TyArrow Type Type deriving (Show,Eq) data Term = TmUnit | TmVar String | TmAbs String Type Term | TmApp Term Term deriving Show {- Context is some LIFO structure which stores Argument-Type bindings: -} data Context = {- ... -} ctxEmpty :: Context addBinding :: Context -> String -> Type -> Context getBinding :: Context -> String -> Type typeof :: Context -> Term -> Type typeof _ TmUnit = TyUnit typeof ctx (TmVar s) = getBinding ctx s typeof ctx (TmAbs s ty1 t) = let ctx' = addBinding ctx s ty1 ty2 = typeof ctx' t in TyArrow ty1 ty2 typeof ctx (TmApp t1 t2) = let (TyArrow ttp tte) = typeof ctx t1 tta = typeof ctx t2 {- (1) problem here: -} in if tta==ttp then tte else error "..." -- eval omitted... The STLC does not provide a notion for recursion as it stands. My idea was to simulate recursion by using infinte structures of type Type. Consider this definition of the omega-combinator: omegaType :: Type omegaType = TyArrow omegaType omegaType omega, omegaAbs :: Term omega = TmApp omegaAbs omegaAbs omegaAbs = TmAbs "x" omegaType (TmApp (TmVar "x") (TmVar "x")) Now it would be nice if "typeof ctxEmpty omega" would return omegaType. Unfortunately it doesn't. Instead it loops on line ((1)), since omegaType and omegaType will never be compared to be equal using (==). If we had a function `sameAddress` we could write "tta `sameAddress` ttp || tta==ttp" instead of "tta==ttp" in line ((1)). If I interpret the chapter about infinite lists in the bird book correctly, this should be sound. omegaType will be represented by a cyclic graph in the runtime system and will therefore always refer to the same cell. The issue becomes a little more complicated if we consider: omegaType, omegaType' :: Type omegaType = TyArrow omegaType omegaType omegaType' = TyArrow omegaType' omegaType' omega, omegaAbs, omegaAbs' :: Term omega = TmApp omegaAbs omegaAbs' omegaAbs = TmAbs "x" omegaType (TmApp (TmVar "x") (TmVar "x")) omegaAbs' = TmAbs "x" omegaType' (TmApp (TmVar "x") (TmVar "x")) In this case it wouldn't be clear whether " omegaType `sameAddress` omegaType' " should be True or False, as a clever compiler might detect that both are identical and make them refer to the same address (, correct me if I'm wrong). This might be a reason that there is no `sameAddress`. My questions are: Is there any way to implement "sameAddress" in Haskell? Or is it at least possible to implement it with GHC using some compiler-specific notation? Thanks, Tim _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
On Sun, Jan 08, 2006 at 12:43:31PM +0100, Tim Walkenhorst wrote:
> {- Disclaimer: I'm rather new to Haskell and completely new to this board. > I may not use the correct terminology in all cases, but I hope my > intention becomes clear when you have a look at the code-snippets. -} > > Hey ho, > > Is there any way two find out whether two variables refer to the > same cell? That is I'm looking for a notion of identity (compareable > to == in Java) as opposed to equality (== in Haskell). If you haven't seen this thread already: "Detecting Cycles in Datastructures" covering exactly your topic, I think.. You can use google groups to find it. It's from okt. Marc _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Tim Walkenhorst-2
On Sunday 08 January 2006 06:43 am, Tim Walkenhorst wrote:
> {- Disclaimer: I'm rather new to Haskell and completely new to this board. > I may not use the correct terminology in all cases, but I hope my > intention becomes clear when you have a look at the code-snippets. -} > > Hey ho, > > Is there any way two find out whether two variables refer to the > same cell? That is I'm looking for a notion of identity (compareable > to == in Java) as opposed to equality (== in Haskell). Another poster has already replied with a link to a long answer. The short answer is "no, not really". An attempted rationale: The semantics of such an "identity" operator are unclear. The operator could be a test for leibenz equality (ie, structural equality, ie replaceability in all contexts), but such an operator cannot be decidable (proof due to Church), so that wouldn't help in your situation anyway. The general usefulness of such an operator is debatable. We could instead provide an implementation-dependent operation that tests for identical heap location, but such an operator would give different results with different Haskell implementations and would be sensitive to optimizations. That would either be a horribly broken operator or (to fix the brokeness) greatly constrain the avaliable optimizations and implementation strategies. For the problem at hand (involving the STLC), you will not be able to type omega because omega is a non-normalizing closed term and STLC has the strong normalization property. You will have to move to a more expressive calculus to type omega. Rob Dockins _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
Thanks for all infos.
I'll apply that Ref-datatype from the "observable sharing" paper to my problem and see where this brings me. I'm also looking into the solution Paul Hudak presented in the "Detecting Cycles in Datastructures" thread in october. > For the problem at hand (involving the STLC), you will not be able to type > omega because omega is a non-normalizing closed term and STLC has the strong > normalization property. You will have to move to a more expressive calculus > to type omega. I guess the infinite omega-"type" I'm using is not a type in the same way as infinity is not a number. You cannot reach it by structural induction. Therefore the strong normalization property will not work for infinite types (or none-types if you prefer). I admit that allowing infinite types basically means moving to a more expressive calculus. Probably the best thing is to introduce the recursion operator mu explicitly and avoid the cyclic structures. I just thought it would be interesting to play around with infinite stuctures in this context. Thanks again, Tim _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
On Monday 09 January 2006 04:09 am, Tim Walkenhorst wrote:
> Thanks for all infos. > > I'll apply that Ref-datatype from the "observable sharing" paper > to my problem and see where this brings me. I'm also looking > into the solution Paul Hudak presented in the > "Detecting Cycles in Datastructures" thread in october. > > > For the problem at hand (involving the STLC), you will not be able to > > type omega because omega is a non-normalizing closed term and STLC has > > the strong normalization property. You will have to move to a more > > expressive calculus to type omega. > > I guess the infinite omega-"type" I'm using is not a type in > the same way as infinity is not a number. You cannot reach it > by structural induction. Right. This is something that seems to cause confusion for people occasionally. I myself didn't understand this subtle point until I did some work with the with the proof assistant Coq which differentiates between inductive and coinductive definitions. Haskell datatypes are actually coinductive, which are are related to sets of objects created by a maximal fixpoint (rather than the more usual least fixpoint). This means that Haskell datatypes admit more values than their inductive cousins, and can cause unintuitive results like this where you can create things that "shouldn't exist" according to the literature, like a type for omega in STLC. > Therefore the strong normalization > property will not work for infinite types (or none-types if > you prefer). I admit that allowing infinite types basically > means moving to a more expressive calculus. Probably the > best thing is to introduce the recursion operator mu explicitly > and avoid the cyclic structures. That would be my recommendation. Cyclic datastructures bend my mind and tend to be hard to work with; I personally try to avoid them except for a few idiomatic uses involving lists. > I just thought it would > be interesting to play around with infinite stuctures in this > context. > > Thanks again, > Tim _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
Free forum by Nabble | Edit this page |