[Haskell-cafe] semantics

[Patrick Browne]

Consider the following definitions:
1. Denotational semantics can be considered as relation between syntax
and mathematical objects (the meaning of the syntax).
2. Operational semantics can be considered as set of rules for
performing computation.

Question 1
Applying these definitions in a Haskell context can I say that the
lambda calculus provides both the operational and denotational
semantics for Haskell programs at value level for definition and
evaluations.

Question 2
Does it make sense to use these definitions at type level? If so, what
exactly do they represent?


Thanks,
Pat

This message has been scanned for content and viruses by the DIT Information 
Services E-Mail Scanning Service, and is believed to be clean. http://www.dit.ie

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] semantics

[Alexander Solla]

On Tue, Feb 8, 2011 at 7:04 AM, Patrick Browne wrote:

> Consider the following definitions:
> 1. Denotational semantics can be considered as relation between syntax
> and mathematical objects (the meaning of the syntax).
> 2. Operational semantics can be considered as set of rules for
> performing computation.
>
> Question 1
> Applying these definitions in a Haskell context can I say that the
> lambda calculus provides both the operational and denotational
> semantics for Haskell programs at value level for definition and
> evaluations.
>
>
Sure.  There are other, more-or-less equally applicable semantic frameworks.
 My preferred framework is:


> Question 2
> Does it make sense to use these definitions at type level? If so, what
> exactly do they represent?
>
>
>
Under the Howard-Curry Isomorphism, the type level definitions correspond to
theorems in a typed logic, and the implementations (the value terms)
correspond to proofs of the theorems.  I suppose this is more of a
"denotational" interpretation.  The language of values and terms is more
operational.

If we really want to try to come up with an operational semantic for types,
I suppose we should start with something along the lines of "a type
represents an 'abstract set' or a 'category' of values.  I suppose some of
these are indexed -- like the functorial types [a], Maybe a, etc.  It is
hard to come up with a single operational semantic for types, because they
do so many different things, and there is a semantic for each
interpretation.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] semantics

[Conal Elliott]

On Tue, Feb 8, 2011 at 7:04 AM, Patrick Browne wrote:

> Consider the following definitions:
> 1. Denotational semantics can be considered as relation between syntax
> and mathematical objects (the meaning of the syntax).
> 2. Operational semantics can be considered as set of rules for
> performing computation.
>
> Question 1
> Applying these definitions in a Haskell context can I say that the
> lambda calculus provides both the operational and denotational
> semantics for Haskell programs at value level for definition and
> evaluations.
>
> Question 2
> Does it make sense to use these definitions at type level? If so, what
> exactly do they represent?
>
> Thanks,
> Pat
>

Here's my personal denotational answer to question 2: I think of a type as
denoting a collection of (mathematical) values. If an expression e has type
T, then the meaning (value) of e is a member of the collection denoted by T.
This simple principle, which is fundamental to how I think of functional
programming, has consequences in library design, which I've discussed at
http://conal.net/blog/posts/notions-of-purity-in-haskell/ .

Regards, - Conal
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] semantics

[kevin]

On Tue, Feb 8, 2011 at 2:01 PM, Alexander Solla  wrote:
> It is hard to come up with a single operational semantic for types, because 
> they do so many different things, and there is a semantic for each 
> interpretation.

G. Hillebrand, P. C. Kanellakis (in paper "Functional Database Query Languages 
as Typed Lambda Calculi of Fixed Order" and others) encoded tuples, lists, 
tables, the relational algebra, complex objects, and others in typed lambda 
calculus. The different things (I guess we can call them types here) were able 
to be compared with the uniformed (opeartional) semantics.



___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] semantics

[kevin]

On Tue, Feb 8, 2011 at 07:55 pm, Conal Elliott  wrote:
Here's my personal denotational answer to question 2: I think of a type as 
denoting a collection of (mathematical) values. If an expression e has type T, 
then the meaning (value) of e is a member of the collection denoted by T. This 
simple principle, which is fundamental to how I think of functional 
programming, has consequences in library design, which I've discussed at 
http://conal.net/blog/posts/notions-of-purity-in-haskell/ .

When we consider a class of partial recursive functions as the type T, then 
what are the expressions (such as e in your statement above) for T?

It seems that the type definition missed operations. For example, if a and b 
are two variables declared as integers, then we would not know how to calculate 
a + b if the type integers didn't include the plus operator.

Defining a type as a set of values and a set of operations on the values is 
perfectly fine mathematically. But in the context of programming languages, a 
type seems to need its syntax anyhow in addition to be a set of values and a 
set of operations on the values. For example the type definition in C:

typedef mydata {
int a;
char c;
}

The definition itself is the syntax while we may view the infinite many records 
{<0, 'a'>, <2, 'a'>, ..., <0, 'b>, } as its semantics (or the semantics was 
called a type earlier).

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] semantics

[Conal Elliott]

On Tue, Feb 8, 2011 at 9:02 PM,  wrote:

>
> On Tue, Feb 8, 2011 at 07:55 pm,  Conal Elliott  wrote:
>
>> Here's my personal denotational answer to question 2: I think of a type as
>> denoting a collection of (mathematical) values. If an expression e has type
>> T, then the meaning (value) of e is a member of the collection denoted by T.
>> This simple principle, which is fundamental to how I think of functional
>> programming, has consequences in library design, which I've discussed at
>> http://conal.net/blog/posts/notions-of-purity-in-haskell/ .
>>
> When we consider a class of partial recursive functions as the type T, then
> what are the expressions (such as e in your statement above) for T?
>

There are many, including application of those functions and to those
functions (in a language with higher-order functions), as well as variables
& primitive constants. The grammar and type system mediates the legal
expressions.


>  It seems that the type definition missed operations. For example, if a and
> b are two variables declared as integers, then we would not know how to
> calculate a + b if the type integers didn't include the plus operator.
>

The original note didn't ask how to assign meanings to expressions, but
denotational semantics (DS) is a clear & simple methodology. Meanings are
defined compositionally. For instance, the meaning of "A + B" is a function
of the meanings of the expressions A and B. Typically, DS is described as
being functions on syntax, but syntax is just one data type, and I find it
very useful for giving semantics to data types, in the same compositional
style. For several examples, see
http://conal.net/papers/type-class-morphisms .

  - Conal


>
> Defining a type as a set of values and a set of operations on the values is
> perfectly fine mathematically. But in the context of programming languages,
> a type seems to need its syntax anyhow in addition to be a set of values and
> a set of operations on the values. For example the type definition in C:
>
> typedef  mydata {
> int a;
> char c;
> }
>
> The definition itself is the syntax while we may view the infinite many
> records {<0, 'a'>, <2, 'a'>, ..., <0, 'b>, } as its semantics (or the
> semantics was called a type earlier).
>
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Semantics for FP?

[Gregory Woodhouse]

First of all, I'm very new to Haskell (but very impressed). I  
remember having a lot of fun with Lisp as an undergrad, and recently  
started working with Scheme (and having a great time at it), and so I  
decided to look into Haskell. Like everyone else, I was totally  
impressed by the two line quicksort -- and hooked.


Unfortunately(?), though, FP seems to pose a bit of a challenge from  
a semantic point of view. I remember being very impressed with  
"Dynamic Logic" (Harel et al.), and it really changed my way of  
thinking about programming languages. But are Kripke structures even  
of any relevance to Haskell and FP? Well, in order to think it  
through, I've been experimenting with the idea of reduction providing  
the basic accessibility relation. That's why I've been asking  
seemingly off-topic questions about lambda calculus and C-R (well- 
definedness).

===
Gregory Woodhouse
[EMAIL PROTECTED]

"The whole of science is nothing more than a refinement
 of everyday thinking."  -- Albert Einstein



___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] semantics of type synonym

[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.


Pat

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Semantics of ForeignPtr Finalizers

[Bas van Dijk]

Hello,

I have a question about the semantics of finalizers of ForeignPtrs:

If an in scope value has a reference to a ForeignPtr is the foreign
object always kept alive, even if that reference is not used? Or do I
always need to wrap each computation, which needs to have the foreign
object alive, inside withForeignPtr?

To make my question more concrete, I will give a simplified example
from my usb library (a high-level binding to the libusb C library):

https://github.com/basvandijk/usb

To use the library you first need to initialize libusb which will
yield a context:

newtype Ctx = Ctx {getCtxFrgnPtr ∷ (ForeignPtr C'libusb_context)}

When you're finished with libusb you need to exit the library. This is
done automatically using a ForeignPtr:

newCtx ∷ IO Ctx
newCtx = mask_ $ do
   ctxPtr ← libusb_init
   Ctx <$> newForeignPtr p'libusb_exit ctxPtr
where
  libusb_init ∷ IO (Ptr C'libusb_context)
  libusb_init = alloca $ \ctxPtrPtr → do
  handleUSBException $ c'libusb_init ctxPtrPtr
  peek ctxPtrPtr

I provide a handy internal utility function for accessing the pointer
to the context:

withCtxPtr ∷ Ctx → (Ptr C'libusb_context → IO α) → IO α
withCtxPtr = withForeignPtr ∘ getCtxFrgnPtr

Because this function uses withForeignPtr it's guaranteed that the
context is kep alive during the duration of the given function. For
example, in the following, it is guaranteed that c'libusb_set_debug is
always given a live context:

setDebug ∷ Ctx → Verbosity → IO ()
setDebug ctx verbosity = withCtxPtr ctx $ \ctxPtr →
   c'libusb_set_debug ctxPtr $ genFromEnum verbosity

There are also types which are derived from a context. For example:
getDevices ∷ Ctx → IO [Device] is a function which given a context
returns a list of USB devices currently attached to your system.

The requirement is that when you need to use a device the context has
to be kept alive. Therefor I keep a reference to the context inside
the device:

data Device = Device
{ getCtx ∷ !Ctx
, getDevFrgnPtr ∷ !(ForeignPtr C'libusb_device)
, deviceDesc ∷ !DeviceDesc
}

The idea is that as long as you have a reference to a device you also
keep the context alive because the device references the context.
(Note that a device, in turn, also contains a ForeignPtr)

getDevices ∷ Ctx → IO [Device]
getDevices ctx = ...
where
  mkDev ∷ Ptr C'libusb_device → IO Device
  mkDev devPtr = liftA2
   (Device ctx)
   (newForeignPtr p'libusb_unref_device devPtr)
   (getDeviceDesc devPtr)

Again I provide a handy internal utility function for accessing the
pointer to a device:

withDevicePtr ∷ Device → (Ptr C'libusb_device → IO α) → IO α
withDevicePtr = withForeignPtr ∘ getDevFrgnPtr

And now my question. Is it guaranteed that when the device is in scope
the context is always kept alive? For example, is the context kept
alive in the following:

openDevice ∷ Device → IO DeviceHandle
openDevice dev = withDevicePtr dev $ \devPtr →
   alloca $ \devHndlPtrPtr → do
 handleUSBException $ c'libusb_open devPtr devHndlPtrPtr
 DeviceHandle dev <$> peek devHndlPtrPtr

Or do I also need to call withCtxPtr inside withDevicePtr as such:

withDevicePtr (Device ctx devFP _) f = withCtxPtr ctx $ \_ →
 withForeignPtr devFP f

Thanks,

Bas

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] semantics of type synonym

[Lutz Donnerhacke]

* 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

[Miguel Mitrofanov]

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

[Tom Davie]

On Tue, Dec 29, 2009 at 2:47 PM, 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.
> 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

[pbrowne]

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

[Miguel Mitrofanov]

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

[Stefan Holdermans]

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

[pbrowne]

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

[Stefan Holdermans]

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

Re: [Haskell-cafe] Semantics of ForeignPtr Finalizers

[wren ng thornton]

On 6/19/11 3:52 AM, Bas van Dijk wrote:
> Hello,
> I have a question about the semantics of finalizers of ForeignPtrs: If
an in scope value has a reference to a ForeignPtr is the foreign object
always kept alive, even if that reference is not used? Or do I always
need to wrap each computation, which needs to have the foreign object
alive, inside withForeignPtr?

I know that the Ptr obtained by withForeignPtr will _not_ keep the foreign
object alive (though withForeignPtr itself will be sure to keep it alive
until the function using the Ptr exits). For instance, this shows up with
ByteStrings if you try to save the Ptr somewhere and then use it after
withForeignPtr exits.

I believe that ForeignPtr itself does promise to keep the foreign object
alive, since it's what holds the finalizers. The documentation claims that
the finalizers are run only once the ForeignPtr becomes unreachable, which
implies that keeping the ForeignPtr is sufficient to keep the foreign
object alive. I haven't used ForeignPtr for truly foreign objects, only
for pseudo-foreign objects like ByteString, but in my experience just
having the ForeignPtr is enough to keep the target alive.

-- 
Live well,
~wren


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Semantics of ForeignPtr Finalizers

[Bas van Dijk]

On 19 June 2011 14:13, wren ng thornton  wrote:
> The documentation claims that
> the finalizers are run only once the ForeignPtr becomes unreachable, which
> implies that keeping the ForeignPtr is sufficient to keep the foreign
> object alive.

Right, that was also my thinking when designing the usb library. What
made me doubt this was the implementation of storable vectors:

http://hackage.haskell.org/packages/archive/vector/0.7.1/doc/html/src/Data-Vector-Storable.html

Note that a storable vector stores both a foreign pointer and a
pointer (presumably so that you don't need to add an offset to the
pointer, inside the foreign pointer, each time you use it):

data Vector a = Vector !(Ptr a) !Int !(ForeignPtr a)

Now, if we follow the above semantics we don't need to call
withForeignPtr when we need to read the memory because the foreign
pointer is referenced by the vector.
However the vector library still calls withForeignPtr. For example:

  basicUnsafeIndexM (Vector p _ fp) i = return
  . unsafeInlineIO
  $ withForeignPtr fp $ \_ ->
peekElemOff p i

So is the withForeignPtr redundant so that this function can be
rewritten to just:

  basicUnsafeIndexM (Vector p _ _) i = return
  . unsafeInlineIO
peekElemOff p i

Regards,

Bas

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Semantics of ForeignPtr Finalizers

[Bas van Dijk]

> On Jun 19, 2011 9:58 AM, "Antoine Latter"  wrote:
>> I'd be afraid of optimizations getting ride of the constructor, and since
>> I'm not using all of the fields I would no longer have a reference to the
>> foreign ptr.
>>
>> Since withForeignPtr touches the foreign pointer the optimizations won't
>> make it go away no matter how it transfoms the function.

Good point.

I already made the necessary fixes to my usb library in the
ForeignPtrFix branch:

https://github.com/basvandijk/usb/tree/ForeignPtrFix

I think I'll merge it with master.

Thanks,

Bas

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Semantics of ForeignPtr Finalizers

[Antoine Latter]

Sending to the list as well.
On Jun 19, 2011 9:58 AM, "Antoine Latter"  wrote:
> On Jun 19, 2011 7:49 AM, "Bas van Dijk"  wrote:
>>
>> On 19 June 2011 14:13, wren ng thornton  wrote:
>> > The documentation claims that
>> > the finalizers are run only once the ForeignPtr becomes unreachable,
> which
>> > implies that keeping the ForeignPtr is sufficient to keep the foreign
>> > object alive.
>>
>> Right, that was also my thinking when designing the usb library. What
>> made me doubt this was the implementation of storable vectors:
>>
>>
>
http://hackage.haskell.org/packages/archive/vector/0.7.1/doc/html/src/Data-Vector-Storable.html
>>
>> Note that a storable vector stores both a foreign pointer and a
>> pointer (presumably so that you don't need to add an offset to the
>> pointer, inside the foreign pointer, each time you use it):
>>
>> data Vector a = Vector !(Ptr a) !Int !(ForeignPtr a)
>>
>> Now, if we follow the above semantics we don't need to call
>> withForeignPtr when we need to read the memory because the foreign
>> pointer is referenced by the vector.
>> However the vector library still calls withForeignPtr. For example:
>>
>> basicUnsafeIndexM (Vector p _ fp) i = return
>> . unsafeInlineIO
>> $ withForeignPtr fp $ \_ ->
>> peekElemOff p i
>>
>> So is the withForeignPtr redundant so that this function can be
>> rewritten to just:
>>
>> basicUnsafeIndexM (Vector p _ _) i = return
>> . unsafeInlineIO
>> peekElemOff p i
>>
>
> I'd be afraid of optimizations getting ride of the constructor, and since
> I'm not using all of the fields I would no longer have a reference to the
> foreign ptr.
>
> Since withForeignPtr touches the foreign pointer the optimizations won't
> make it go away no matter how it transfoms the function.
>
> Antoine
>
>> Regards,
>>
>> Bas
>>
>> ___
>> 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

[Haskell-cafe] Semantics of uniqueness types for IO (Was: Why can't Haskell be faster?)

[apfelmus]

Stefan Holdermans wrote:

Exposing uniqueness types is, in that sense, just an alternative
to monadic encapsulation of side effects.  


While  *World -> (a, *World)  seems to work in practice, I wonder what 
its (denotational) semantics are. I mean, the two programs


  loop, loop' :: *World -> ((),*World)

  loop  w = loop w
  loop' w = let (_,w') = print "x" w in loop' w'

both have denotation _|_ but are clearly different in terms of side 
effects. (The example is from SPJs awkward-squad tutorial.) Any pointers?


Regards,
apfelmus

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Semantics of uniqueness types for IO (Was: Why can't Haskell be faster?)

[Arnar Birgisson]

Hi there,

I'm new here, so sorry if I'm stating the obvious.

On Nov 1, 2007 2:46 PM, apfelmus <[EMAIL PROTECTED]> wrote:
> Stefan Holdermans wrote:
> > Exposing uniqueness types is, in that sense, just an alternative
> > to monadic encapsulation of side effects.
>
> While  *World -> (a, *World)  seems to work in practice, I wonder what
> its (denotational) semantics are. I mean, the two programs
>
>loop, loop' :: *World -> ((),*World)
>
>loop  w = loop w
>loop' w = let (_,w') = print "x" w in loop' w'
>
> both have denotation _|_ but are clearly different in terms of side
> effects. (The example is from SPJs awkward-squad tutorial.) Any pointers?

For side-effecting program one has to consider bisimilarity. It's
common that semantically equivalent (under operational or denotational
semantics) behave differently with regard to side-effects (i/o) - i.e.
they are not bisimilar.

http://en.wikipedia.org/wiki/Bisimulation

Arnar
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Semantics of uniqueness types for IO (Was: Why can't Haskell be faster?)

[Paul Hudak]

One can certainly use an operational semantics such
as bisimulation, but you don't have to abandon denotational semantics. 
The trick is to make output part of the "final answer".  For a
conventional imperative language one could define, for example, a
(lifted, recursive) domain:

Answer = Terminate + (String x Answer)

and then define a semantic function "meaning", say, such that:

meaning loop = _|_
meaning loop' = <"x", <"x", ... >>

In other words, loop denotes bottom, whereas loop' denotes the infinite
sequence of "x"s.  There would typically also be a symbol to denote
proper termination, perhaps <>.

A good read on this stuff is Reynolds book "Theories of Programming
Languages", where domain constructions such as the above are called
"resumptions", and can be made to include input as well.

In the case of Clean, programs take as input a "World" and generate a
"World" as output.  One of the components of that World would
presumably be "standard output", and that component's value would be
_|_ in the case of loop, and <"x",
<"x", ... >> in the case of loop'.  Another part of the World
might be a file system, a printer, a missile firing, and so on. 
Presumably loop and loop' would not affect those parts of the World.

If returning one World is semantically problematical, one might also
devise a semantics where the result is a sequence of Worlds.

    -Paul


Arnar Birgisson wrote:

  Hi there,

I'm new here, so sorry if I'm stating the obvious.

On Nov 1, 2007 2:46 PM, apfelmus <[EMAIL PROTECTED]> wrote:
  
  
Stefan Holdermans wrote:


  Exposing uniqueness types is, in that sense, just an alternative
to monadic encapsulation of side effects.
  

While  *World -> (a, *World)  seems to work in practice, I wonder what
its (denotational) semantics are. I mean, the two programs

   loop, loop' :: *World -> ((),*World)

   loop  w = loop w
   loop' w = let (_,w') = print "x" w in loop' w'

both have denotation _|_ but are clearly different in terms of side
effects. (The example is from SPJs awkward-squad tutorial.) Any pointers?

  
  
For side-effecting program one has to consider bisimilarity. It's
common that semantically equivalent (under operational or denotational
semantics) behave differently with regard to side-effects (i/o) - i.e.
they are not bisimilar.

http://en.wikipedia.org/wiki/Bisimulation

Arnar





___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe