Re: [Haskell-cafe] semantics of type synonym
* pbrowne wrote: semantics). I used the following type synonym: type String = [Char] type Name = String String, Name and [Char] are synonyms, which means every expression is identically to the others. There is no difference besides that String and Name are type aliases while [Char] is a type construct. getName :: String - Name getName n = n I checked the types with two tests: -- test 1 :t ww ww :: [Char] The type interference system determines that you have an array of characters, hence a [Char]. All those existing type aliases are suppressed by the module. Otherwise the list get's very long ... -- test 2 :t getName(ww) getName(ww) :: Name From the definition of getName, the compiler knows which type alias is prefered from the set of equivalent names. Obviously I get two different types. You get two different representations of the same type. In the case of the function Haskells type system seems to pick up enough information to determine that “ww” is a Name. Nope. ww is still a [Char] for the compiler. And you do not even check for the type of ww. :t snd . (\x - (getName x, x)) $ ww ... :: String ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] semantics of type synonym
pbrowne wrote: Hi, I am studying the underlying semantics behind Haskell and to what degree those semantics are actually implemented. I need to clarify what a *type synonym* actual means in relation to Haskell's logic (or formal semantics). I used the following type synonym: type Name = String getName(n) = n I checked the types with two tests: -- test 1 :t ww ww :: [Char] -- test 2 :t getName(ww) getName(ww) :: Name Obviously I get two different types. Wrong. You get exactly the same type, it's just that GHCi detected that you have a fancy name for this type, so it gives you that name. It's not type system, it's just GHCi. In the case of the function Haskells type system seems to pick up enough information to determine that “ww” is a Name. But I am not sure what is happening with the literal ww in the first test. Pat ___ 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] semantics of type synonym
On Tue, Dec 29, 2009 at 2:47 PM, pbrowne patrick.bro...@comp.dit.ie wrote: Hi, I am studying the underlying semantics behind Haskell and to what degree those semantics are actually implemented. I need to clarify what a *type synonym* actual means in relation to Haskell's logic (or formal semantics). I used the following type synonym: type Name = String getName(n) = n I checked the types with two tests: -- test 1 :t ww ww :: [Char] -- test 2 :t getName(ww) getName(ww) :: Name Obviously I get two different types. In the case of the function Haskells type system seems to pick up enough information to determine that “ww” is a Name. But I am not sure what is happening with the literal ww in the first test. This isn't really Haskell doing anything, but a particular implementation... In Haskell a type synonym is *exactly* that – Name is indistinguishable from String, which in turn is indistinguishable from [Char]. The compiler/interpretter is free to return any one of them as it choses. What's happening here is that ghci(?) is returning the one it thinks is most likely to be familiar to you. Bob ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] semantics of type synonym
Hi, It seems that I need to distinguish between a theory for Haskell and a given implementation (GHCi). I have two further queries based on the replies; 1) Obviously I get two different types Wrong. You get exactly the same type, it's just that GHCi detected that you have a fancy name for this type, so it gives you that name. It's not type system, it's just GHCi. Are you saying there is just one type? (not two isomorphic types because there is only one of them with two names) 2) In the case of the function Haskells type system seems to pick up enough information to determine that “ww” is a Name. Nope. ww is still a [Char] for the compiler. And you do not even check for the type of ww. :t snd . (\x - (getName x, x)) $ ww ... :: String Why are the GHCi commands :t ww and :t getName(ww) not a valid type checks? Pat pbrowne wrote: Hi, I am studying the underlying semantics behind Haskell and to what degree those semantics are actually implemented. I need to clarify what a *type synonym* actual means in relation to Haskell's logic (or formal semantics). I used the following type synonym: ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] semantics of type synonym
1) Obviously I get two different types Wrong. You get exactly the same type, it's just that GHCi detected that you have a fancy name for this type, so it gives you that name. It's not type system, it's just GHCi. Are you saying there is just one type? (not two isomorphic types because there is only one of them with two names) Exactly the same. You can take a term of one of these types and feed it to the function expecting another, and visa versa. 2) In the case of the function Haskells type system seems to pick up enough information to determine that “ww” is a Name. Nope. ww is still a [Char] for the compiler. And you do not even check for the type of ww. :t snd . (\x - (getName x, x)) $ ww ... :: String Why are the GHCi commands :t ww and :t getName(ww) not a valid type checks? They are. Pat pbrowne wrote: Hi, I am studying the underlying semantics behind Haskell and to what degree those semantics are actually implemented. I need to clarify what a *type synonym* actual means in relation to Haskell's logic (or formal semantics). I used the following type synonym: ___ 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] semantics of type synonym
Patrick, It seems that I need to distinguish between a theory for Haskell and a given implementation (GHCi). What do you mean by this? Obviously I get two different types Wrong. You get exactly the same type, it's just that GHCi detected that you have a fancy name for this type, so it gives you that name. It's not type system, it's just GHCi. Are you saying there is just one type? (not two isomorphic types because there is only one of them with two names) Indeed. To create a new type isomorphic to an existing type, have a look at newtype declarations. (http://www.haskell.org/onlinereport/decls.html , §4.2). Why are the GHCi commands :t ww and :t getName(ww) not a valid type checks? I am not sure what you mean by this. Cheers, Stefan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] semantics of type synonym
Stefan Holdermans wrote: It seems that I need to distinguish between a theory for Haskell and a given implementation (GHCi). What do you mean by this? From the responses to my query, it seems that I cannot rely totally on the compiler for my research question which is concerned with the meaning of Haskell constructs I will have to consult the Haskell Report. Why are the GHCi commands :t ww and :t getName(ww) not a valid type checks? I am not sure what you mean by this. l...@iks-jena.de wrote; And you do not even check for the type of ww. :t snd . (\x - (getName x, x)) $ ww ... :: String From the above, I though perhaps that my checks were not valid tests for the type of the expressions. Thanks, Pat ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] semantics of type synonym
Dear Patrick, From the responses to my query, it seems that I cannot rely totally on the compiler for my research question which is concerned with the meaning of Haskell constructs I will have to consult the Haskell Report. For both practical and theoretical matters, GHC provides a very decent implementation of the Haskell 98 standard. Divergences from the standard are minor and properly documented: http://www.haskell.org/ghc/docs/latest/html/users_guide/bugs-and-infelicities.html#vs-Haskell-defn . HTH, Stefan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
