Constructors on left and right hand sides of equation
Dear list In Eq 1 is (NewGlass i) on the LHS distinct from (NewGlass i) on the RHS? In Eq2 are the occurrences of the data constructor Fill on the LHS and RHS distinct? Thanks Pat data Glass = NewGlass Int | Fill Glass Int deriving Show drink :: Glass -> Int -> Glass drink (NewGlass i) j = (NewGlass i) -- Eq 1 drink (Fill m i) j | full (Fill m i) = Fill (NewGlass (size m)) ((size m) - j) -- Eq 2 | (i >= j) = Fill m (i-j) | otherwise = drink m (j-1) size :: Glass -> Int size (NewGlass i) = i size (Fill m i) = size m level :: Glass -> Int level (NewGlass i) = 0 level (Fill m i) | (level m) + i > (size m) = size m | otherwise = (level m) + i empty :: Glass -> Bool empty m = (level m) == 0 full :: Glass -> Bool full m = (level m) == (size m) {- drink (Fill (NewGlass 4) 5) 5 drink (Fill (NewGlass 4) 3) 3 -} -- This email originated from DIT. If you received this email in error, please delete it from your system. Please note that if you are not the named addressee, disclosing, copying, distributing or taking any action based on the contents of this email or attachments is prohibited. www.dit.ie Is ó ITBÁC a tháinig an ríomhphost seo. Má fuair tú an ríomhphost seo trí earráid, scrios de do chóras é le do thoil. Tabhair ar aird, mura tú an seolaí ainmnithe, go bhfuil dianchosc ar aon nochtadh, aon chóipeáil, aon dáileadh nó ar aon ghníomh a dhéanfar bunaithe ar an ábhar atá sa ríomhphost nó sna hiatáin seo. www.dit.ie Tá ITBÁC ag aistriú go Gráinseach Ghormáin – DIT is on the move to Grangegorman http://www.dit.ie/grangegorman
PATRICK BROWNE
drink (NewGlass i) j = (NewGlass i) -- Eq 1
In Eq 1 is (NewGlass i) on the LHS distinct from (NewGlass i) on the RHS?
drink (Fill m i) j | full (Fill m i) = Fill (NewGlass (size m)) ((size m) - j) -- Eq2
In Eq2 are the occurrences of the data constructor Fill on the LHS and RHS distinct?
Yes they're distinct. This is important since their types can be different. Here's an extreme example:
data Proxy a = Proxy
foo :: Proxy Int -> Proxy Bool foo Proxy = Proxy
It looks like "foo" is the identity function, returning its argument value, similar to these "bar" functions:
bar1 :: () -> () bar1 () = ()
bar2 :: () -> () bar2 = id
However, it's not:
foo2 :: Proxy Int -> Proxy Bool foo2 = id
[1 of 1] Compiling Main ( test.hs, interpreted )
test.hs:7:8: Couldn't match type `Int' with `Bool' Expected type: Proxy Int -> Proxy Bool Actual type: Proxy Int -> Proxy Int In the expression: id In an equation for `foo2': foo2 = id Failed, modules loaded: none.
Hence, in general, we must assume that they're different values. We tend to use different terminology too, for example "patterns" on the left, "expressions" on the right; "destructing" on the left, "constructing" on the right. Cheers, Chris
On 18/09/2014, at 2:03 AM, PATRICK BROWNE wrote:
Dear list In Eq 1 is (NewGlass i) on the LHS distinct from (NewGlass i) on the RHS? In Eq2 are the occurrences of the data constructor Fill on the LHS and RHS distinct?
data Glass = NewGlass Int | Fill Glass Int deriving Show drink :: Glass -> Int -> Glass drink (NewGlass i) j = (NewGlass i) -- Eq 1 drink (Fill m i) j | full (Fill m i) = Fill (NewGlass (size m)) ((size m) - j) -- Eq 2 | (i >= j) = Fill m (i-j) | otherwise = drink m (j-1)
The question question is "what do you MEAN by 'are they distinct'"? They are two distinct references to a single binding occurrence of an identifier. In Eq1, the first occurrence is in a pattern, and the second is in an expression. I wonder if you were interested in the question whether the second occurrence of NewGlass i would allocate new storage or whether it would use whatever the first occurrence matched? In that case, I believe the answer is "it's up to the compiler". You can *ask* for the matched data to be shared: drink g@(NewGlass _) _ = g drink g@(Fill m i ) j | full g = Fill (NewGlass (size m)) (size m - j) | i >= j = Fill m (i - j) | True = drink m (j - 1) Someone else has already pointed out data Proxy a = Proxy -- foo :: Proxy a -> Proxy b foo Proxy = Proxy -- Eq3 where the two occurrences of Proxy in Eq3 can have different types. But note that -- bar :: Proxy a -> Proxy a bar p@Proxy = p -- Eq4 The two occurrences of the variable p in Eq4 must have the same type (and the same value).
On Thu, Sep 18, 2014 at 4:08 AM, Richard A. O'Keefe
On 18/09/2014, at 2:03 AM, PATRICK BROWNE wrote:
Dear list In Eq 1 is (NewGlass i) on the LHS distinct from (NewGlass i) on the RHS? In Eq2 are the occurrences of the data constructor Fill on the LHS and RHS distinct?
data Glass = NewGlass Int | Fill Glass Int deriving Show drink :: Glass -> Int -> Glass drink (NewGlass i) j = (NewGlass i) -- Eq 1 drink (Fill m i) j | full (Fill m i) = Fill (NewGlass (size m)) ((size m) - j) -- Eq 2 | (i >= j) = Fill m (i-j) | otherwise = drink m (j-1)
The question question is "what do you MEAN by 'are they distinct'"?
They are two distinct references to a single binding occurrence of an identifier. In Eq1, the first occurrence is in a pattern, and the second is in an expression.
I wonder if you were interested in the question whether the second occurrence of NewGlass i would allocate new storage or whether it would use whatever the first occurrence matched? In that case, I believe the answer is "it's up to the compiler". You can *ask* for the matched data to be shared:
drink g@(NewGlass _) _ = g drink g@(Fill m i ) j | full g = Fill (NewGlass (size m)) (size m - j) | i >= j = Fill m (i - j) | True = drink m (j - 1)
Someone else has already pointed out
data Proxy a = Proxy
-- foo :: Proxy a -> Proxy b foo Proxy = Proxy -- Eq3
where the two occurrences of Proxy in Eq3 can have different types. But note that
-- bar :: Proxy a -> Proxy a bar p@Proxy = p -- Eq4
The two occurrences of the variable p in Eq4 must have the same type (and the same value).
Since we're talking about allocating new storage: even though 'Eq3' has a second occurrence of 'Proxy' on the right hand side, I believe in GHC's implementation these are shared and there is only one Proxy at runtime. Of course this is implementation dependent. Regards, Erik
On 18 September 2014 03:08, Richard A. O'Keefe
The question question is "what do you MEAN by 'are they distinct'"?
They are two distinct references to a single binding occurrence of an identifier. In Eq1, the first occurrence is in a pattern, and the second is in an expression.
Thanks for the feedback. If both occurrences of (NewGlass i) in Eq1 reference the same object in memory then I would consider them to be the same. If they reference different objects I would consider them to be equal but not the same. Is (Fill m i ) in Eq 2 a type constructor? Is it treated the same as the data constructor (NewGlass i)? -- This email originated from DIT. If you received this email in error, please delete it from your system. Please note that if you are not the named addressee, disclosing, copying, distributing or taking any action based on the contents of this email or attachments is prohibited. www.dit.ie Is ó ITBÁC a tháinig an ríomhphost seo. Má fuair tú an ríomhphost seo trí earráid, scrios de do chóras é le do thoil. Tabhair ar aird, mura tú an seolaí ainmnithe, go bhfuil dianchosc ar aon nochtadh, aon chóipeáil, aon dáileadh nó ar aon ghníomh a dhéanfar bunaithe ar an ábhar atá sa ríomhphost nó sna hiatáin seo. www.dit.ie Tá ITBÁC ag aistriú go Gráinseach Ghormáin – DIT is on the move to Grangegorman http://www.dit.ie/grangegorman
On 18/09/2014, at 7:56 PM, PATRICK BROWNE wrote:
Thanks for the feedback. If both occurrences of (NewGlass i) in Eq1 reference the same object in memory then I would consider them to be the same. If they reference different objects I would consider them to be equal but not the same. Is (Fill m i ) in Eq 2 a type constructor? Is it treated the same as the data constructor (NewGlass i)?
Let's repeat the original code. data Glass -- missing comment = NewGlass Int -- missing comment | Fill Glass Int -- missing comment deriving Show drink :: Glass -> Int -> Glass drink (NewGlass i) j = (NewGlass i) -- Eq 1 drink (Fill m i) j | full (Fill m i) = Fill (NewGlass (size m)) ((size m) - j) -- Eq 2 | i >= j = Fill m (i-j) | otherwise = drink m (j-1) First, (Fill m i) isn't *any* kind of constructor. Second, the first occurrence of (Fill m i) is a (data) pattern containing the (data) constructor Fill, and the second occurrence of (Fill m i) is an expression containing the (data) constructor Fill. We may not know what Glass, NewGlass, and Fill *mean*, but we know what they *are* (as Haskell thingies). There are no objects, and "are these the same object" is not a question that can meaningfully be asked about values in a Haskell program. (It IS a question that CAN meaningfully be asked about the related language Clean, because Clean has, or is alleged to have, a semantics in terms of graph rewriting, where "node in graph" is not entirely unlike "object".) As has been previously noted, two occurrences of "the same" term need not have the same type. I have often been tripped up by this: emap :: (a -> b) -> Either String a -> Either String b emap _ (Left msg) = Left msg emap f (Right val) = Right (f val) works but emap _ e@(Left msg) = e emap f (Right val) = Right (f val) does not work because the two occurrences of Left msg have different types. When the two occurrences *do* have the same type, it is up to the compiler to decide whether they will refer to the same place in memory or whether a copy will be made. There is no test you can perform in Haskell to distinguish. (It's the same in Prolog and Erlang and SML and F#.) If it comes to that, consider a much simpler question. f :: Integer -> Integer f 123456789123456789123456789 = 123456789123456789123456789 f _ = error "just an example" Are the two occurrences of that big integer "the same"? Who knows? How could you tell? Now consider g :: (Char,Int) -> (Char,Int) g pair@(_,_) = pair I would like to tell you that multiple occurrences of the same *variable* refer to a single copy of the data value, but I can't find anything in the Haskell report to guarantee this. Maybe I didn't look hard enough.
On 19 September 2014 06:05, Richard A. O'Keefe
drink (NewGlass i) j = (NewGlass i) -- Eq 1 drink (Fill m i) j | full (Fill m i) = Fill (NewGlass (size m)) ((size m) - j) -- Eq 2 | i >= j = Fill m (i-j) | otherwise = drink m (j-1)
First, (Fill m i) isn't *any* kind of constructor. Second, the first occurrence of (Fill m i) is a (data) pattern containing the (data) constructor Fill, and the second occurrence of (Fill m i) is an expression containing the (data) constructor Fill. We may not know what Glass, NewGlass, and Fill *mean*, but we know what they *are* (as Haskell thingies).
Your response has clarified most of my confusion. Please bear with my naivety as seek to ride my mind of confusion over these two point: 1) I do not know what the phrase "(Fill m i) isn't *any* kind of constructor." means. 2) Does "Fill (NewGlass (size m)) ((size m) - j) " create two Glass Haskell thingies? The context of this code is an attempt to formalize the drinking operation[1]. [1] www.ncgia.ucsb.edu/Publications/Tech_Reports/95/95-7.pdf -- This email originated from DIT. If you received this email in error, please delete it from your system. Please note that if you are not the named addressee, disclosing, copying, distributing or taking any action based on the contents of this email or attachments is prohibited. www.dit.ie Is ó ITBÁC a tháinig an ríomhphost seo. Má fuair tú an ríomhphost seo trí earráid, scrios de do chóras é le do thoil. Tabhair ar aird, mura tú an seolaí ainmnithe, go bhfuil dianchosc ar aon nochtadh, aon chóipeáil, aon dáileadh nó ar aon ghníomh a dhéanfar bunaithe ar an ábhar atá sa ríomhphost nó sna hiatáin seo. www.dit.ie Tá ITBÁC ag aistriú go Gráinseach Ghormáin – DIT is on the move to Grangegorman http://www.dit.ie/grangegorman
participants (4)
-
Chris Warburton -
Erik Hesselink -
PATRICK BROWNE -
Richard A. O'Keefe