been calculated the function uses this information to
define equality on values of type object via equality on values of type
name.
Benjamin Franksen wrote:
pbrowne wrote:
Dependent Types (DT)
The purpose of dependent types (DT) is to allow programmers to specify
dependencies between
Hi,
I am attempting to explain an example of dependent types to computing
practitioners who do not have any background in functional programming.
My goal is to explain the example rather than implement or improve it. I
have been told in previous postings that the approach below is a bit
dated. Any
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
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
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
pbrowne wrote:
2) What, if anything, prevents the execution of a Haskell term from
being a proof in equational logic?
I have done some checking to try to answer my own question. The answer
*seems* to be that there *seems* to be three things that prevent Haskell
terms being true equations. Any
The issue of *purity* in Haskell and this thread has confused me.
At value level (not type level) is this linked with *equational reasoning*?
Are the operational semantics of Haskell similar but not the same as
equational logic?
Why are theorem provers such as Haskabelle need?
Dan,
From your example, I can appreciate the value of purity. But I am still
unsure how close Haskell terms are to pure *equational logic*[1]. The
operational semantics of languages like CafeOBJ[1] are very close to
their intended logical semantics. CafeOBJ modules contain theories in
equational
Luke Palmer wrote:
I admit that I don't fully know what you are talking about. What do
you mean by logical meaning -- as opposed to what other sort of
meaning?
Consider Maude's rewrite logic RWL[1] which has similar inference rules
as equational logic(EL), but without the symmetry rule. From
Luke Palmer lrpal...@gmail.com wrote
I feel like this should be qualified. Type classes are not for name
punning ; you wouldn't use a type class for the method bark on types
Tree and Dog. But if you have a well-defined *structure* that many
types follow, then a type class is how you capture
o...@okmij.org wrote:
Brent Yorgey wrote:
John Reynolds showed long ago that any higher-order language can be
encoded in first-order. We witness this every day: higher-order
language like Haskell is encoded in first-order language (machine
code). The trick is just to add a layer of
11 matches
Mail list logo
