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. 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:
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
* 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
On Tue, Dec 29, 2009 at 2:47 PM, pbrowne
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
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:
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)
information to determine that “ww” is a Name. Nope. "ww" is still a [Char] for the compiler. And you do not even check for
In the case of the function Haskells type system seems to pick up enough 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
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
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.
lutz@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
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-infelicitie... . HTH, Stefan
On Tue, 2009-12-29 at 14:47 +0000, 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
Don't use parentheses. You can think it looks like function call oin other languages but it is not. (n) is a "one-element tuple" i.e. n so if you have function with 2 arguments f (n, k) will not work (it will apply one argument which is a tuple). usually it is written as: getName n = n or getName = id
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.
Pat
ghci> :t getName "ww" getName "ww" :: [Char] ghci> :t getName "ww" :: [Char] getName "ww" :: [Char] :: [Char] ghci> :t (getName "ww" :: [Char]) :: String (getName "ww" :: [Char]) :: String :: String ghci> :t ((getName "ww" :: [Char]) :: String) :: Name ((getName "ww" :: [Char]) :: String) :: Name :: Name it works only because [Char], String and Name are synonimes (:: works differently then () cast in C/C++ where (int)((double)((int)0)) is legal). As far as compiler/interpreter is concerned it is indifferent on the exact naming. However it tried to guess what name You would like to have. For example: type FullPath = String type RelativePath = String expand :: RelativePath -> FullPath expand = ... it is much more clear what you get (FullPath) - not just the raw type. Of course it will not stop you when you state expand . expand as it is rather decorative thing. If you want to create new type you need to write: newtype Name = Name String Regards
participants (6)
-
Lutz Donnerhacke -
Maciej Piechotka -
Miguel Mitrofanov -
pbrowne -
Stefan Holdermans -
Tom Davie