Is a second order type one whose instances (values?) are ordinary types?Are kinds *-* second order types?Is Species without the argument a second order type?But with the argument Species is a first order type?Thanks,Pat-- Elephant and Dog typesdata Elephant = Elephant deriving Showdata Dog = Dog
HiIs it reasonable to consider a Haskell class as a loose signature-only-specification (denoting a theory) and an instance as an implementation (denoting a model)?In the example below the specification of the class BUILDING is textually smaller than the specification of the class HOUSE,provided we
Hi,The code [1] below compiles and runs with GHCi version 7.0.4.I get one warning and an error message with GHCi version 7.6.1.1) Warning -XDatatypeContexts is deprecated. Unless there are propagation effects, this is well explained.2) foom-1.hs:65:15: `quality' is applied to too many type
-7-4-1.html#id3015054Roman* Patrick Browne patrick.bro...@dit.ie [2013-07-09 12:45:19+0100] Hi, The code [1] below compiles and runs with GHCi version 7.0.4. I get one warning and an error message with GHCi version 7.6.1. 1) Warning -XDatatypeContexts is deprecated. Unless
On 30/06/13, Dan Burton danburton.em...@gmail.com wrote:I am not trying to say every building is a shelter, rather anything that is a building must provide sheltering services.
Well if it walks like a shelter and quacks like a shelter... /shrugOne of the nice things about OO is the
intuitive
:46 PM, Patrick Browne wrote:Hi,The runtime behaviour of the two modules below *seems* to be the same.Is this correct? I am not trying to say every building is a shelter, rather anything that is a building must provide sheltering services.I think that the use of sub-classes makes this explicit
. For this all to work out, it also means that any instance of B must be coupled with an instance for A.Does this help clarify?RichardOn Jun 30, 2013, at 1:46 PM, Patrick Browne wrote:As you say if I omit references to superclass methods in the subclasses then I get different compile time behaviour.But
Hi,The runtime behaviour of the two modules below *seems* to be the same.Is this correct? I am not trying to say every building is a shelter, rather anything that is a building must provide sheltering services.I think that the use of sub-classes makes this explicit, but it *seems* that one gets
, does not mean higher mathematical abstraction, but to be closer to the way the mind works.
2013/5/15 Patrick Browne patrick.bro...@dit.ie patrick.bro...@dit.ie
-- Hi-- I am trying to show that a set of propositions and a conclusion the form a valid argument.-- I used two approaches; 1) using
-- Hi-- I am trying to show that a set of propositions and a conclusion the form a valid argument.-- I used two approaches; 1) using if-then-else, 2) using pattern matching.-- The version using if-then-else seems to be consistent with my knowledge of Haskell and logic (either of which could be
/Theorem_provers
and http://en.wikipedia.org/wiki/Automated_theorem_provinghope it helps
On Wed, May 15, 2013 at 11:34 AM, Patrick Browne patrick.bro...@dit.ie patrick.bro...@dit.ie wrote:
-- Hi-- I am trying to show that a set of propositions and a conclusion the form a valid argument.-- I used two
{-I am trying to apply model theoretic concepts to Haskell by considering type classes as theories and instances as models.Then the declaration of a sub-class specifies a signature morphism from the superclass to the subclass.In case below the theories (classes) are signature only (no default
On 23/08/12, Brent Yorgey byor...@seas.upenn.edu wrote:fun1 returns 8 for all inputs. The fact that fun1's definition usesthe name 'constant' which happens to have the same name as somethingin scope is irrelevant. For example, this is precisely the same as the above:constant :: Intconstant =
On 09/08/12, Jay Sulzberger j...@panix.com wrote:Here we are close to the distinction between a class of objectswhich satisfy a condition vs objects with added structure, forwhich see: http://math.ucr.edu/home/baez/qg-spring2004/discussion.html
Gast [1] describes a 3 level hierarchy of Haskell objects using elementOf from set theory:value *elementOf* type *elementOf* classQuestionIf we include super-classes would the following be an appropriate mathematical representation?value *elementOf* type *elementOf* class *subSet*
On 08/08/12, Ertugrul Söylemez e...@ertes.de wrote: If we include super-classes would the following be an appropriate mathematical representation?What is a superclass? What are the semantics?I assume that like a normal class a super-class *defines* a set operations for types, but it is not *a
On 08/08/12, Ertugrul Söylemez e...@ertes.de wrote:So you basically just mean class (Functor f) = Applicative fYes, but I want to know if there is a simple mathematical relation between the classes and/or their typesBut from your emails the original hierarchy seems to have been superseded,
Ertugrul,Thank you for your detailed and helpful reply.I was unaware of the distinction between data/value and type constructors.Regards,PatOn 31/07/12, Ertugrul Söylemez e...@ertes.de wrote:Patrick Browne patrick.bro...@dit.ie wrote: Thanks for all the very useful feed back on this thread. I
am not sure what guarantees the compiler makes about unsafeCoerce.
-- ryanOn Sun, Jul 22, 2012 at 7:19 AM, Patrick Browne patrick.bro...@dit.ie patrick.bro...@dit.ie wrote:
{-Below is a *specification* of a queue. If possible I would like to write the equations in type class.Does the type class
{- I am trying to understand and provide a *simplified* explanation of instance contexts and their relationship with class hierarchies. I use the example from [1]. Are the following two sentences and annotated code a reasonable explanation? When instantiating an instance I of C, its context must
On 22/07/12, Ertugrul Söylemez e...@ertes.de wrote:You are probably confusing the type class system with something fromOOP. A type class captures a pattern in the way a type is used. Thecorresponding concrete representation of that pattern is then written inthe instance definition: No really.
add any kind of special constructors as functions in the type class which return a new queue. For example:
class Stack s where newEmptyStack :: s a newSingletonStack :: a - s a ...Why doesn't this fulfill you needs of specifying ways to construct new elements?
2012/7/23 Patrick Browne
Dominique,That is exactly the information that I required.Thank you very much,PatOn 23/07/12, Dominique Devriese dominique.devri...@cs.kuleuven.be wrote:Patrick, -- Class with functional dependency class QUEUE_SPEC_CLASS2 a q | q - a where newC2 :: q a -- ?? sizeC2 :: q a - Int restC2
{-Below is a *specification* of a queue. If possible I would like to write the equations in type class.Does the type class need two type variables? How do I represent the constructors?Can the equations be written in the type class rather than the instance?-}module QUEUE_SPEC wheredata Queue e =
Ertugrul ,Thanks for you very clear explanation.Without committing to some concrete representation such as list I do
not know how to specify constructors in the class (see below). As you point out a class may not be appropriate for an actual application, but I am investigating the strengths and
Hi,I am comparing Haskell's class/instance techniques for overloading with those available Order Sorted Algebra (OSA in CafeOBJ) Using just the basic class/instance mechanism is there any way to avoid the type annotations in the evaluations below?Patclass Location a b where move::a-binstance
Hi, I apologize if the formatting or content of my previous email caused offence. Hopefully my question is better phrased and presented this time. Below is my attempt to code the first example from Walder’s Theorems for free! paper[1]. {-# LANGUAGE ExistentialQuantification #-} import
Hi,
Below is my attempt to code the first example from Walder’s Theorems for
free! paper.
I am not sure about what is being proved.
Using the notation from the paper does the proof establish a
property of map, r, composition or the relationship between all three?
{-# LANGUAGE
matter whether you apply the map functionbefore or after applying the r itself.Hope that helps,Wojciech2012/2/27 Patrick Browne patrick.bro...@dit.ie: Hi, Below is my attempt to code the first example from Walder’s Theorems for free! paper. I am not sure about what is being proved. Using the notation
at 10:12 AM, Patrick Browne patrick.bro...@dit.ie patrick.bro...@dit.ie wrote:
On 21/12/11, Richard O'Keefe o...@cs.otago.ac.nz o...@cs.otago.ac.nz wrote:
So what exactly is the program supposed to do?
I am trying to see whether Haskell modules can be used for
blending[1]. The original MAUDE [2,3
On 21/12/11, Richard O'Keefe o...@cs.otago.ac.nz wrote:So what exactly is the program supposed to do?
I am trying to see whether Haskell modules can be used for
blending[1]. The original MAUDE [2,3]
program just sets up an arbitrary meeting point, which is assumed to be time-2
and location-2.
Hi,I am trying to implement a set of 4 modules that blend the action of a monk moving up a mountain on day 1 and returning down by the same path on day 2 [1][2]. The code should reflect the fact that there is some time and place which is common to the two days where the monk would *meets himself*.
On 12/20/11, Paul Johnson p...@cogito.org.uk wrote:I think you need to rethink the solution: Haskell is not a logic programming language.
Yes of
course, but I suspect that the problems are due to issues of scope and modularity rather than problems of a logical nature
The main
equation for
On 12/20/11, Paul Johnson p...@cogito.org.uk wrote:You definitely don't need the type class, and you don't need instances.I have removed the type class and instances.I have placed the location function in MONKONMOVEUP and MONKONMOVEDOWNNow I can at least access the functions and some of values.
I have simplified the code using constructors and export.I can evalute the qualified expressions but I do not get the expected results.module MONKONMOVE (module MONKONMOVE)wheredata Monk = Monk | Monku | Monkd deriving (Show,Eq)data TimeOfDay = TimeOfDay | Timeu1 | Timeu2 | Timeu3 | Timed1 |
Is there a partial order on Haskell type classes?If so, does it induce any quasi-order relation on types named in the instances?In the example below types C and D have the same operation fThanks,Patdata C = C deriving Showdata D = D deriving Showclass A t where f::t-t f t = t instance A C
Hi,I am comparing some aspects of Haskell with Java.Below is a simple Haskell program with a sub-class.It is followed my attempt to code the same concepts in Java.Two questions:1) Are the two examples close enough? (very subjective)2) In this example, what are the advantages of the Haskell type
Hi,Does the subclass relation have any meaning when two classes have instances with the same type?I get the same results from Listing 1 and Listing 2 below.Regards,Pat-- Listing 1- Subclassdata Shed = Shed class Building building where addressB :: building - Integer addressB b = 1--
Hi,
Does the subclass relation have any meaning when two classes have instances with the same type?
I get the same results from Listing 1 and Listing 2 below.
Regards,
Pat
-- Listing 1- Subclass
data Shed = Shed
class Building building where
addressB :: building - Integer
addressB b =
In the current example does the following totally or partially ignore the type class system.boo :: Shed - Integerboo h = addressB h + addressH hOn 16/10/11, Daniel Fischer daniel.is.fisc...@googlemail.com wrote:In your example, the only difference is that with the superclass constraintfoo ::
Hi,
Below are two questions concerning overloading in a sub-class.
Thanks,
Pat
class Numb0 a where
(+) :: a - a - a
negate :: a - a
instance Numb0 Int where
x + y = y
negate x = x
-- Are + and negate part of the signature of Numb1?
class Numb0 a = Numb1 a where
-- Is it possible to
typeclasses a type is a
member of, use :info.
On 12/08/2011 23:52, Patrick Browne wrote:
Hi,
Why does the Haskell :type command only sometimes print the type-class?
Should I expect type-class inference as well as type inference?
Maybe the type-class is inferred where possible, but not always
Hi,
Why does the Haskell :type command only sometimes print the type-class?
Should I expect type-class inference as well as type inference?
Maybe the type-class is inferred where possible, but not always printed?
Thanks,
Pat
-- Code
k x = x + 3
data T = T
class A a where
g::a - a
g a = a
Below are examples of using the sub-class context at class level and at instance level. In this simple case they seem to give the same resultsIn general, are there certain situations in which one or the other is preferred? Patmodule CLASS where-- class and sub-classclass Class a where foo :: a - a
What is the difference between using a class context and deriving in
data type declaration?
Are there certain situations in which one or the other is preferred?
data Eq a = Set1 a = NilSet1 | ConsSet1 a (Set1 a)
data Set2 a = NilSet2 | ConsSet2 a (Set2 a) deriving Eq
(NilSet1) ==
Hi,
Below are some questions about the logical interpretation of types and
type classes.
Thanks,
Pat
module J where
type Id = String
type Position = Integer
data Person = Person Id Position deriving Show
-- Is this an axiom at type level?
class Pos a where
getPos :: a - Position
-- The :type
Is it possible to access type information and perform either of the
following in a Haskell program?
1) Find the type/class of a variable
e.g. a type predicate: is y of-type A, or is y of-Class A
2) Assert the type of a variable
e.g. if y.length 100 then y is of type big.
Regards,
Pat
This
On 22/07/2011 10:18, Patrick Browne should have wrote:
2) Assert the class of a variable
e.g. if y.length 100 then y is of class big.
Regards,
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
On 18/07/2011 13:52, Ketil Malde wrote:
I'm not sure the question makes sense, if fly is a method of class
Bird, then it can't also be a member of class Penguin.
I am actually doing a language comparison and I was checking out a paper
that said:
Type classes allow for partial inheritance, so
On 18/07/2011 19:14, Jerzy Karczmarczuk wrote:
That's why I suggested how you might do that: for some datatypes, say
the Emperors, you specify some special flying method (e.g. dummy or
bombing), or you don't specify it at all. And the Emperors won't fly.
-- Here is my attempt
data Emperor =
Hi,
My understanding of the constructor discipline (CD) is that it is a
restriction on the form of an equation that guarantees that the equation
represents an executable function. The CD restricts the LHS of an
equation to consist of a function name, constructors, and variables.
Also there should
Hi,
Is it possible to model partial inheritance using Haskell type classes?
For example, if the class Bird has a flying method can we represent
Penguins as a sub-class of Bird without a flying method?
Regards,
Pat
This message has been scanned for content and viruses by the DIT Information
Hi,
I am trying to understand the following code.
I have written my current (mis-)understanding and questions below.
I do not wish to improve the code, it is from a research paper[1] that I
am trying to understand.
Pat
[1] ftp://ftp.geoinfo.tuwien.ac.at/medak/phdmedak.pdf
-- A specification. The
How do I make an instance of the Vehicles class below?
Thanks,
Pat
class Containers x y where
insert :: y - x y - x y
remove :: y - x y - x y
whatsIn :: x y - [y]
instance Containers [] Char where
insert y [] = y:[]
insert y m = y:m
remove _ [] = []
remove x (y:ys) |
On 12/06/2011 10:43, MigMit wrote:
I fail to understand why instantiating a four-argument class with five
arguments seems obvious to you.
class (Surfaces v o, Paths a b (v o)) = Vehicles v o a b where
Obviously I am wrong! But my incorrect thinking is as follows:
Surfaces takes 2 arguments,
Thanks for the feedback. I have two further questions
1. Why is it that the Containers class signature does not allow
instances to be list of list? I suspect it is because x is a constructor.
2. How would I change the Containers class signature to allow instances
to be lists of lists.
Thanks,
Hi
Below is a class that I wish to create some instances of.
I do not wish to change the class definition.
It is supposed to represent containers of type x that contain things of
type y.
My attempt at the insert function seems ok for Char and lists, but not
ok for Integer. How do I instantiate
Are casts required to run the code below?
If so why?
Thanks,
Pat
-- Idetifiers for objects
class (Integral i) = IDs i where
startId :: i
newId :: i - i
newId i = succ i
sameId, notSameId :: i - i - Bool
-- Assertion is not easily expressible in Haskell
-- notSameId i newId i = True
sameId
Are the following two functions equivalent? (i.e. do they describe the
same computation)
let add1 a = a + 2
let add2 = \ a - a + 2
:t add1
add1 :: forall a. (Num a) = a - a
:t add2
add2 :: forall a. (Num a) = a - a
Does Haskell interpreter convert all functions in the form of add1 to
the
Continuing the thread on model expansion.
I have changed the example trying to focus on expanding models of M in G
Why is the operation ! ok or RHS but not visible on LHS of G?
The equation itself does not seem to suffer from the dependent type
problem of my previous post.
class M a where
(!)
-- inverse a ! a = e
You can also specify a QuickCheck property:
propInverse :: (Eq a, Group a) = a - Bool
propInverse a = (inverse a ! a) == e
I've put up an example on hpaste at http://hpaste.org/47234/simple_monoid
-- ryan
On Sat, May 28, 2011 at 2:46 AM, Patrick Browne
Hi,
I'm not sure if this is possible but I am trying to use Haskell’s type
class to specify *model expansion*. Model expansion allows the
specification of new symbols (known as enrichment) or the specification
further properties that should hold on old symbols. I am trying to
enrich simplified
On 10/04/2011 04:22, wren ng thornton wrote:
The thing is that a lot of the common optimizations (e.g., TCO)
completely wreck the inductive structure of the function which, in turn,
makes it difficult to say interesting things about them.[1]
Could you point me to some Haskell references
Hi,
Attached are two programs that represent one-way and two-way traffic on
a road. I can get the programs to produce reasonable results that match
our intuitive ideas of roads.
However, I have 2 question about the programs:
1)I cannot get the result suggested by the author that t1 should give
start)) (Node end)
=gives= Node start
Or we can begin at the start and end at the end.
other (Edge (Node start) (Node end)) (Node start)
=gives= Node end
So prog1 allows a car to go in both directions.
Pat
On 03/04/2011 15:39, Daniel Fischer wrote:
On Sunday 03 April 2011 16:04:22, Patrick
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
Hi,
I am studying type classes using examples from the literature [1].
The attached code is a formalization of basic object oriented ideas. The
particular approach seems to be built on the concepts of: thing, object,
and identifier.
I have no intension to implement anything or significantly change
On 29/01/2011 20:56, Henning Thielemann wrote:
Is there a reason why you use an individual type for every unit?
The existing implementations of typed physical units only encode the
physical dimension in types and leave the unit factors to the value
level. I found this to be the most natural
On 30/01/2011 19:43, Henning Thielemann wrote:
I do not see a constant 1 that is equated with a type.
This is due to my misunderstanding of Haskell.
After your comments my understanding of the unit function is as follows:
1) In the instance below the argument for unit must have type
Ryan,
This is exactly what I was looking for.
Thanks,
Pat
On 20/01/2011 18:56, Ryan Ingram wrote:
On Wed, Jan 19, 2011 at 11:56 PM, Patrick Browne patrick.bro...@dit.ie
wrote:
I am trying to see what how this requirement can be represented using
just the normal instance-implements-class
On 19/01/2011 10:41, Ryan Ingram wrote:
It's still not really clear what you are trying to do.
I am trying to see what how this requirement can be represented using
just the normal instance-implements-class relation for a comparison with
a specification language approach.
If there is no simple
-- My intension is that the PERSON class should *specify*
-- that a person has a constant id called p1
-- and that a person has a name that can be found from the id.
class PERSON a b where
p1 :: a
name :: a - b
-- My intension is that the instance should implement the PERSON class
instance
Henning,
The code is not intended to fit into a larger application.
I am trying to understand instance-implements-class relation.
My experiment consists of writing simple English sentences and then
seeing how they could be specified and implemented in Haskell.
I am sure that this simple
On 17/01/2011 13:04, Ketil Malde wrote:
So other PERSONs would have different types, say:
I think the problem is there is just one constant p1 in the class and
there needs to be multiple constants in the implementation (one for each
person). It seems difficult to specify this using type classes
14:07, Patrick Browne wrote:
On 17/01/2011 13:04, Ketil Malde wrote:
So other PERSONs would have different types, say:
I think the problem is there is just one constant p1 in the class and
there needs to be multiple constants in the implementation (one for each
person). It seems difficult
On 22/12/2010 14:48, Artyom Shalkhakov wrote:
..Do you want to prove a property of
a function formally, using some kind of formal logic?
I am aware that functional languages do not do proofs at term level, but
the motivation for my question is to get a precise reason why this is
so. The replies
Hi,
In a previous posting[1] I asked was there a way to achieve a proof of
mirror (mirror x) = x
in Haskell itself. The code for the tree/mirror is below:
module BTree where
data Tree a = Tip | Node (Tree a) a (Tree a)
mirror :: Tree a - Tree a
mirror (Node x y z) = Node (mirror z) y
On 31/10/2010 16:55, Brent Yorgey wrote:
Note that the first parameter to commutative shadows the previous
definition of com, I don't know if that's what you intended.
Does the following avoid the shadowing?
infixl 5 `op`
op :: Int - Int - Int
x `op` y = (x + y)
commutative op1 = \a b - (a
Hi,
Below are two questions on commutative operations in Haskell.
infixl 5 `com`
com :: Int - Int - Int
x `com` y = (x + y)
commutative com a b = (a `com` b) == (b`com`a)
-- 1 + 3 == 3 + 1
-- This gives true by virtue of the value of LHS and RHS being equal
after the plus operation
-- Question
Hi,
I hypothesize that at type level Haskell offers a form of equational
logic. At type level the following program[1] could be interpreted as a
first order program in equational logic where;
1)Data types represent declarations of constructors (both constants and
functions)
2)Type synonyms
Patrick,
Thanks for taking the time to get the program running.
It seems fine, but I cannot get the *md* to print out, probably missing
the Show class somewhere.
Thanks again,
Pat
Patrick LeBoutillier wrote:
Patrick,
I found this program interesting and decided to spend a bit of time on
hi,
I am trying to run and understand a lifting program from [1].
The program lifts points to moving points that vary their position over
time.
I made some effort to run the progrm but I do not know how to overide
the +,-,*,sqr, and sqrt from the Num class. Below is my current attempt.
I do not
Alexander Solla wrote:
Doing similar constructions with type classes is possible. I think you
might have to use witness types (or even a nice functorial wrapper
around your target value in the original algebra, or both) to do
generalizations of type classes. For example:
class Uneditable
Alexander Solla wrote:
On 09/26/2010 01:32 PM, Patrick Browne wrote:
Bigger how? Under logical implication and its computational analogue?
That is to say, do you want the model to be more SPECIFIC, describing a
smaller class of objects more richly (i.e, with more logical
implications
Hi,
Below is an assumption (which could be wrong) and two questions.
ASSUMPTION 1
Only smaller models can be specified using the sub-class mechanism.
For example if we directly make a subclass A = B then every instance of
B must also be an instance of A (B implies A or B is a subset of A).
Hence,
Hi,
The details of the issues involved in an open and closed facility for
Haskell are way beyond my current understanding of the language.
Nonetheless, I was wondering does this have anything to do with the
expression problem?
Pat
17/08/2010 14:48 Victor Nazarov asviraspossi...@gmail.com wrote:
Daniel Fischer wrote:
class BEING human = HUMAN human where
Sub-classing is logical implication BEING(human) = HUMAN(human)
All types t that make BEING(t) = true also make HUMAN(t)=true
No, it's the other way round. Every HUMAN is also a BEING, hence
HUMAN(t) = BEING(t)
Could I say
Hi,
I am trying to understand type classes and sub-classes in purely logical
terms From the literature I gather that:
1)a type class is a predicate over types (using type variables)
2)type sub-classing is a logical implication between these predicates.
But I feel that 1) and 2) does not give
Sebastian,
Thanks for your very useful reply.
Does the EQ example below not talk about inhabited types as proofs.
Thanks,
Pat
Sebastian Fischer wrote:
If we find a value for a type that is a proof that a type exists (it is
inhabited) that is a member of the class
I don't understand the
Hi,
The expression problem [1] can be described as the ability to add new
variants (either constructors or methods) to a data type without
changing the existing code. The Haskell and OO language issues are well
described at [1]
It seems that the expression problem does not exist in Maude[2].
My
Andrew,
Thanks for your detailed feedback, it is a great help.
I appreciate that the code does not do anything useful, nor is it an
appropriate way to write Haskell, but it does help me
understand language constructs. I have seen statements like
data C3 c3 a = Address c3 a = Address c3 a
and
Hi,
I am studying the Haskell type class system as part of a language
comparison thesis. At this point I am looking at how default function
definitions are handled in classes. Functions are usually defined in
instances, not classes. I appreciate that the code below may not be an
appropriate way to
Hi,
I am trying to understand the data type declaration below.
What is the relation between class C3 and the data type Address below?
Where is such a technique used?
Thanks,
Pat
module A where
data Person = Person String Integer deriving Show
data Employee = Employee String Integer deriving
Patrick Browne wrote:
Hi,
In Haskell what roles are played by 1)lambda calculus and 2) equational
logic? Are these roles related?
I think this thread is getting a bit too theoretical, so I moved it to
http://lambda-the-ultimate.org/node/4014
Thanks for putting the time and effort into your
Heinrich Apfelmus wrote:
Lambda calculus is the basis for all three types of semantics:
1) Call-by-need (usually, implementations of Haskell are free to choose
other evaluation strategies as long as the denotational semantics match)
2) The denotational semantics of a lambda calculus
In Haskell what roles are played by 1)lambda calculus and 2) equational
logic? Are these roles related?
Hi,
Thanks for your clear and helpful responses.
I am aware that this question can lead to into very deep water.
I am comparing Haskell with languages based on equational logic (EL)
(e.g.
Hi,
In Haskell what roles are played by 1)lambda calculus and 2) equational
logic? Are these roles related?
Hopefully this question can be answered at a level suitable for this forum.
Thanks,
Pat
This message has been scanned for content and viruses by the DIT Information
Services E-Mail
Hi,
I would like to understand the Peano module below.
I do wish to implement or improve the code.
I am unsure of the semantics of (suc = Suc) and then the subsequent use
of (Suc n)
Is this an example of type-level programming?
module Peano where
data Nat = Zero | Suc Nat deriving Show
class
Hi,
My understanding of functional dependencies is that they can be used to
ensure that one type depends on another type.
For example, the type of location depends could on the type of the
object at that location.
Consider two models
1) The location of an aircraft landing should have location of
one type, which causes a problem.
Thanks for the quick and informative response,
Pat
Neil Brown wrote:
On 01/07/10 12:37, Patrick Browne wrote:
Why do some cases such as 1) fail to run even if they are the only
instantiation.
-- 1) Compiles but does not run
instance LocatedAt Int String
100 matches
Mail list logo
