[Haskell-cafe] ANN: WFLP 2010 Call for participation
Call For Participation WFLP2010 19th International Workshop on Functional and (Constraint) Logic Programming Madrid, Spain, January 17, 2010 http://babel.ls.fi.upm.es/events/wflp2010/ * colocated with Principles of Programming Languages POPL 2010 http://www.cse.psu.edu/popl/10/ IMPORTANT DATES Hotel reservation deadline: December 28, 2009 VENUE WFLP2010 and all POPL'10 affiliated events will take place at the Melia Castilla Hotel, Madrid. REGISTRATION To register for WFLP2010, follow the link from the POPL 2010 page, at http://www.cse.psu.edu/popl/10/ SCOPE The aim of the Workshop on Functional and (Constraint) Logic Programming is to bring together researchers interested in functional programming and (constraint) logic programming with special emphasis on the integration of both paradigms and of other declarative programming extensions. It promotes the cross-fertilizing exchange of ideas and experiences among researchers and students from the different communities interested in the foundations, applications, and combinations of high-level declarative programming languages and related areas. INVITED SPEAKER Mariangiola Dezani (University of Torino, Italy) ACCEPTED PAPERS Transforming Functional Logic Programs into Monadic Functional Programs Bernd Brassel, Sebastian Fischer, Michael Hanus and Fabian Reck Mixed-level Embedding and JIT Compilation for an Iteratively Staged DSL George Giorgidze and Henrik Nilsson An Access Control Language based on Term Rewriting and Description Logic Michele Baggi, Demis Ballis and Moreno Falaschi Lazy and Faithful Assertions for Functional Logic Programs Michael Hanus Parameterized Models for On-line and Off-line Use Pieter Wuille and Tom Schrijvers A Denotational Semantics for Curry Jan Christiansen, Daniel Seidel and Janis Voigtlander A Declarative Debugger of Missing Answers for Functional and Logic Programming Rafael del Vado Virseda and Fernando Perez Morente Efficient and Compositional Higher-Order Streams Gergely Patai Bridging the gap between two Concurrent Constraint Languages Alexei Lescaylle Daudinot and Alicia Villanueva Garcia Large scale random testing with QuickCheck on MapReduce framework Shigeru Kusakabe and Yuuki Ikuta Automated verification of security protocols in tccp Alexei Lescaylle Daudinot and Alicia Villanueva Garcia Implementation and Evaluation of a Declarative Debugger for Java Herbert Kuchen and Christian Hermanns PROGRAM CHAIR Julio Marino (Universidad Politecnica de Madrid, Spain) PROGRAM COMMITTEE Maria Alpuente (Universidad Politecnica de Valencia, Spain) Sergio Antoy (Portland State University, USA) Bernd Brassel (CAU Kiel, Germany) Olaf Chitil (Univ. of Kent, UK) Rachid Echahed (CNRS-IMAG, France) Santiago Escobar (Universidad Politecnica de Valencia, Spain) Moreno Falaschi (Universita di Siena, Italy) Murdoch Gabbay (Heriot-Watt University, UK) Maria Garcia de la Banda (Monash University, Australia) Victor Gulias (Lambdastream SL, Spain) Michael Hanus (CAU Kiel, Germany) Herbert Kuchen (Univ. of Muenster, Germany) Francisco Lopez-Fraguas (Universidad Complutense de Madrid, Spain) James Lipton (Wesleyan University, USA) Mircea Marin (Univ. of Tsukuba, Japan) Juan Jose Moreno-Navarro (Ministry of Science Innovation, Spain) Brigitte Pientka (McGill University, Canada) Call For Participation WFLP2010 19th International Workshop on Functional and (Constraint) Logic Programming Madrid, Spain, January 17, 2010 http://babel.ls.fi.upm.es/events/wflp2010/ * colocated with Principles of Programming Languages POPL 2010 http://www.cse.psu.edu/popl/10/ IMPORTANT DATES Hotel reservation deadline: December 28, 2009 VENUE WFLP2010 and all POPL'10 affiliated events will take place at the Melia Castilla Hotel, Madrid. REGISTRATION To register for WFLP2010, follow the link from the POPL 2010 page, at http://www.cse.psu.edu/popl/10/ SCOPE The aim of the Workshop on Functional and (Constraint) Logic Programming is to bring together researchers interested in functional programming and (constraint) logic programming with special emphasis on the integration of both paradigms and of other declarative programming extensions. It promotes the
[Haskell-cafe] Final CFP: WFLP 2010. Deadlines extended: Abstract due Nov 18; Full paper due Nov 25 (LNCS)
[Deadlines extended: Abstract due Nov 18; Full paper due Nov 25] Final Call For Papers 19th International Workshop on Functional and (Constraint) Logic Programming Madrid, Spain, January 17, 2010 http://babel.ls.fi.upm.es/events/wflp2010/ * colocated with Principles of Programming Languages POPL 2010 http://www.cse.psu.edu/popl/10/ IMPORTANT DATES Abstract Submission: November 18, 2009 **extended** Full Paper Submission: November 25, 2009 **extended** Acceptance Notification: December 20, 2009 Preliminary Proceedings: January 7, 2010 Workshop: January 17, 2010 SCOPE The aim of the Workshop on Functional and (Constraint) Logic Programming is to bring together researchers interested in functional programming and (constraint) logic programming with special emphasis on the integration of both paradigms and of other declarative programming extensions. It promotes the cross-fertilizing exchange of ideas and experiences among researchers and students from the different communities interested in the foundations, applications, and combinations of high-level declarative programming languages and related areas. The previous WFLP editions are: WFLP 2009 (Brasilia, Brazil), WFLP 2008 (Siena, Italy), WFLP 2007 (Paris, France), WFLP 2006 (Madrid, Spain), WCFLP 2005 (Tallinn, Estonia), WFLP 2004 (Aachen, Germany), WFLP 2003 (Valencia, Spain), WFLP 2002 (Grado, Italy), WFLP 2001 (Kiel, Germany), WFLP 2000 (Benicassim, Spain), WFLP'99 (Grenoble, France), WFLP'98 (Bad Honnef, Germany), WFLP'97 (Schwarzenberg, Germany), WFLP'96 (Marburg, Germany), WFLP'95 (Schwarzenberg, Germany), WFLP'94 (Schwarzenberg, Germany), WFLP'93 (Rattenberg, Germany), and WFLP'92 (Karlsruhe, Germany). LOCATION WFLP 2010 will be held on January 17, 2010 in Madrid, Spain, colocated with the 37th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL 2010). WFLP 2010 solicits papers in all areas of functional and (constraint) logic programming, including but not limited to: * Foundations: formal semantics, logic variables, binding and abstract syntax, rewriting and narrowing, unification, constraint solving, dynamics, type theory, meta-theory, effects, etc. * Language Design: security, services, modules, type systems, multi-paradigm languages, concurrency and distribution, objects, libraries, generic programming, interoperability, etc. * Implementation: abstract machines, parallelism, compile-time and run-time optimizations, foreign-language interfaces, memory management, multi-threading, exploiting parallel hardware, etc. * Transformation and Analysis: abstract interpretation, specialization, partial evaluation, program transformation, program calculation, program proof, meta-programming, generative programming, etc. * Software Development: algorithms, data structures, design patterns, components and composition, specification, proof assistants, verification and validation, model checking, debugging, testing, profiling, tracing, etc. * Paradigm Integration: integration of declarative programming with other paradigms or features such as imperative, object-oriented, aspect-oriented, concurrent, real-time programming, event-driven architectures, etc. * Applications: education, industry, commercial uses, domain-specific languages, visual/graphical user interfaces, embedded systems, WWW applications, XML processing, artificial intelligence, knowledge representation and machine learning, deductive databases, advanced programming environments and tools, etc. SUBMISSIONS and PROCEEDINGS Authors are invited to submit papers presenting original unpublished work. Papers must be at most 15 pages long. Exceptionally, authors may surpass the page limit by providing well-marked appendices intended as reviewing aids. Appendices will not appear in the final publication. Submission categories include regular research papers, system descriptions, and short papers describing on-going work (at most 8 pages). Submissions must be formatted in Lecture Notes in Computer Science (LNCS) style. This requirement needs not apply to appendices. Papers should be submitted in pdf format electronically via the web-based submission site http://www.easychair.org/conferences/?conf=wflp2010 Preliminary proceedings will be available at the workshop. Selected authors will be invited to submit a full version of their papers after the workshop. Contributions accepted for the post-workshop proceedings will be published in Springer's Lecture Notes in Computer Science series. INVITED SPEAKER Mariangiola Dezani (University of
[Haskell-cafe] ANN: WFLP2010 2nd CFP: LNCS + invited speaker + abstract due Nov 9
Second Call For Papers 19th International Workshop on Functional and (Constraint) Logic Programming Madrid, Spain, January 17, 2010 http://babel.ls.fi.upm.es/events/wflp2010/ * colocated with Principles of Programming Languages POPL 2010 http://www.cse.psu.edu/popl/10/ IMPORTANT DATES Abstract Submission: November 9, 2009 Full Paper Submission: November 15, 2009 Acceptance Notification: December 15, 2009 Preliminary Proceedings: January 5, 2010 Workshop: January 17, 2010 SCOPE The aim of the Workshop on Functional and (Constraint) Logic Programming is to bring together researchers interested in functional programming and (constraint) logic programming with special emphasis on the integration of both paradigms and of other declarative programming extensions. It promotes the cross-fertilizing exchange of ideas and experiences among researchers and students from the different communities interested in the foundations, applications, and combinations of high-level declarative programming languages and related areas. The previous WFLP editions are: WFLP 2009 (Brasilia, Brazil), WFLP 2008 (Siena, Italy), WFLP 2007 (Paris, France), WFLP 2006 (Madrid, Spain), WCFLP 2005 (Tallinn, Estonia), WFLP 2004 (Aachen, Germany), WFLP 2003 (Valencia, Spain), WFLP 2002 (Grado, Italy), WFLP 2001 (Kiel, Germany), WFLP 2000 (Benicassim, Spain), WFLP'99 (Grenoble, France), WFLP'98 (Bad Honnef, Germany), WFLP'97 (Schwarzenberg, Germany), WFLP'96 (Marburg, Germany), WFLP'95 (Schwarzenberg, Germany), WFLP'94 (Schwarzenberg, Germany), WFLP'93 (Rattenberg, Germany), and WFLP'92 (Karlsruhe, Germany). LOCATION WFLP 2010 will be held on January 17, 2010 in Madrid, Spain, colocated with the 37th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL 2010). WFLP 2010 solicits papers in all areas of functional and (constraint) logic programming, including but not limited to: * Foundations: formal semantics, logic variables, binding and abstract syntax, rewriting and narrowing, unification, constraint solving, dynamics, type theory, meta-theory, effects, etc. * Language Design: security, services, modules, type systems, multi-paradigm languages, concurrency and distribution, objects, libraries, generic programming, interoperability, etc. * Implementation: abstract machines, parallelism, compile-time and run-time optimizations, foreign-language interfaces, memory management, multi-threading, exploiting parallel hardware, etc. * Transformation and Analysis: abstract interpretation, specialization, partial evaluation, program transformation, program calculation, program proof, meta-programming, generative programming, etc. * Software Development: algorithms, data structures, design patterns, components and composition, specification, proof assistants, verification and validation, model checking, debugging, testing, profiling, tracing, etc. * Paradigm Integration: integration of declarative programming with other paradigms or features such as imperative, object-oriented, aspect-oriented, concurrent, real-time programming, event-driven architectures, etc. * Applications: education, industry, commercial uses, domain-specific languages, visual/graphical user interfaces, embedded systems, WWW applications, XML processing, artificial intelligence, knowledge representation and machine learning, deductive databases, advanced programming environments and tools, etc. SUBMISSIONS and PROCEEDINGS Authors are invited to submit papers presenting original unpublished work. Papers must be at most 15 pages long. Exceptionally, authors may surpass the page limit by providing well-marked appendices intended as reviewing aids. Appendices will not appear in the final publication. Submission categories include regular research papers, system descriptions, and short papers describing on-going work (at most 8 pages). Submissions must be formatted in Lecture Notes in Computer Science (LNCS) style. This requirement needs not apply to appendices. Papers should be submitted in pdf format electronically via the web-based submission site http://www.easychair.org/conferences/?conf=wflp2010 Preliminary proceedings will be available at the workshop. Selected authors will be invited to submit a full version of their papers after the workshop. Contributions accepted for the post-workshop proceedings will be published in Springer's Lecture Notes in Computer Science series. INVITED SPEAKER Mariangiola Dezani (University of Torino, Italy) PROGRAM CHAIR Julio Marino (Universidad Politecnica de Madrid, Spain) PROGRAM
[Haskell-cafe] ANN: WFLP 2010 Call for papers
[Apologies for multiple receptions of this message] Preliminary Call For Papers 19th International Workshop on Functional and (Constraint) Logic Programming Madrid, Spain, January 17, 2010 http://babel.ls.fi.upm.es/events/wflp2010/ * colocated with Principles of Programming Languages POPL 2010 http://www.cse.psu.edu/popl/10/ IMPORTANT DATES Abstract Submission: November 9, 2009 Full Paper Submission:November 15, 2009 Acceptance Notification: December 15, 2009 Preliminary Proceedings: January 5, 2010 Workshop: January 17, 2010 SCOPE The aim of the Workshop on Functional and (Constraint) Logic Programming is to bring together researchers interested in functional programming and (constraint) logic programming with special emphasis on the integration of both paradigms and of other declarative programming extensions. It promotes the cross-fertilizing exchange of ideas and experiences among researchers and students from the different communities interested in the foundations, applications, and combinations of high-level declarative programming languages and related areas. The previous WFLP editions are: WFLP 2009 (Brasilia, Brazil), WFLP 2008 (Siena, Italy), WFLP 2007 (Paris, France), WFLP 2006 (Madrid, Spain), WCFLP 2005 (Tallinn, Estonia), WFLP 2004 (Aachen, Germany), WFLP 2003 (Valencia, Spain), WFLP 2002 (Grado, Italy), WFLP 2001 (Kiel, Germany), WFLP 2000 (Benicassim, Spain), WFLP'99 (Grenoble, France), WFLP'98 (Bad Honnef, Germany), WFLP'97 (Schwarzenberg, Germany), WFLP'96 (Marburg, Germany), WFLP'95 (Schwarzenberg, Germany), WFLP'94 (Schwarzenberg, Germany), WFLP'93 (Rattenberg, Germany), and WFLP'92 (Karlsruhe, Germany). LOCATION WFLP 2010 will be held on January 17, 2010 in Madrid, Spain, colocated with the 37th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL 2010). WFLP 2010 solicits papers in all areas of functional and (constraint) logic programming, including but not limited to: * Foundations: formal semantics, logic variables, binding and abstract syntax, rewriting and narrowing, unification, constraint solving, dynamics, type theory, meta-theory, effects, etc. * Language Design: security, services, modules, type systems, multi-paradigm languages, concurrency and distribution, objects, libraries, generic programming, interoperability, etc. * Implementation: abstract machines, parallelism, compile-time and run-time optimizations, foreign-language interfaces, memory management, multi-threading, exploiting parallel hardware, etc. * Transformation and Analysis: abstract interpretation, specialization, partial evaluation, program transformation, program calculation, program proof, meta-programming, generative programming, etc. * Software Development: algorithms, data structures, design patterns, components and composition, specification, proof assistants, verification and validation, model checking, debugging, testing, profiling, tracing, etc. * Paradigm Integration: integration of declarative programming with other paradigms or features such as imperative, object-oriented, aspect-oriented, concurrent, real-time programming, event-driven architectures, etc. * Applications: education, industry, commercial uses, domain-specific languages, visual/graphical user interfaces, embedded systems, WWW applications, XML processing, artificial intelligence, knowledge representation and machine learning, deductive databases, advanced programming environments and tools, etc. SUBMISSIONS and PROCEEDINGS Authors are invited to submit papers presenting original unpublished work. Papers must be at most 15 pages long. Exceptionally, authors may surpass the page limit by providing well-marked appendices intended as reviewing aids. Appendices will not appear in the final publication. Submission categories include regular research papers, system descriptions, and short papers describing on-going work (at most 8 pages). Submissions must be formatted in Lecture Notes in Computer Science (LNCS) style. This requirement needs not apply to appendices. Papers should be submitted in pdf or postscript format electronically via the web-based submission site http://www.easychair.org/conferences/?conf=wflp2010 Preliminary proceedings will be available at the workshop. Selected authors will be invited to submit a full version of their papers after the workshop. Contributions accepted for the post-workshop proceedings have usually appeared in journals -- those of the 2009 edition have been published in LNCS, previous editions in ENTCS, etc. PROGRAMME
Re: [Haskell-cafe] Using fundeps to resolve polymorphic types to concrete types
[0] [EMAIL PROTECTED]:~/test $ ghc --version The Glorious Glasgow Haskell Compilation System, version 6.8.2 I have an older version and wonder what goes wrong. Now that I think of it, other stuff that I coudn't compile might actually work in 6.8 It does make sense that |b| is resolved to |B| because of the functional dependency. P. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Using fundeps to resolve polymorphic types to concrete types
Wren ng thornton wrote: It compiles just fine with (DeriveType A b = b - b) after all, which resolves directly to (B - B) That's not the case: simpleNarrow :: DeriveType A b = b - b simpleNarrow = id Couldn't match expected type `b' (a rigid variable) against inferred type `B' `b' is bound by the type signature for `simpleNarrow' ... When using functional dependencies to combine DeriveType A B, arising from the instance declaration ... DeriveType A b, arising from is bound by the type signature for `simpleNarrow' ... I think Bryan got the order in which type inference/checking works wrong. The dependency is not resolved before calculating the type as he suggested. *Main someDestructor (SomeConstructor undefined undefined :: ComplexType A) B Why not this: *Main someDestructor (SomeConstructor A B) B But if you have actual values rather than just unit types, note that this won't work: instance DeriveType A B where someDestructor (SomeConstructor _ b) = b I couldn't understand the sentence actual values rather than unit types. What do you have in mind? P. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Using fundeps to resolve polymorphic types to concrete types
But if you have actual values rather than just unit types, note that this won't work: instance DeriveType A B where someDestructor (SomeConstructor _ b) = b I couldn't understand the sentence actual values rather than unit types. What do you have in mind? I didn't pay attention to the |b| value returned. So what you meant was that only a constant function will do, not a function that returns the value |b|. P. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A type signature inferred by GHCi that is rejected when written explicitly
I myselft don't understand why GHCi doesn't accept the type it infered as an explicit signature ... I think it has to do with the following: Looking at the type errors, they seem to indicate that the type checker is being general and does not assume the |From| and |To| relations are between a type |t| and (s (t x) x)| but, in general, between |t| and |s (t' x) x|. Given that from :: (From a1 c1 x) = a1 x - c1 x to :: (To a2 c2 y) = c2 y - a2 y bimap :: Bifunctor s = (t1 - t3) - (t2 - t4) - s t1 t2 - s t3 t4 During type checking the following equations spring up: c2 y = s t3 t4 c1 x = s t1 t2 t2 = x t4 = y t1 = a1 x t3 = a2 y That'd give the same type as that inferred, but somehow new variables |a11| and |a12| appear. caused by a lack of functional dependencies. class From a c x | a - c where class To a c y | c - a where ... hushes GHCi. The question now is, of course, if the new dependencies are too restrictive for your problem. They are of little avail given the instances I define: instance Bifunctor s = From (Fix s) (s (Fix s x)) x where from = out instance Bifunctor s = To (Fix s) (s (Fix s y)) y where to = In ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] extensible data types in Haskell?
I prefer Bruno's approach, though. It allows meta-level type-checking
of expressions and there's the possibility of closing the extension
with a wrapper:
(References: Generics as a Library and his PhD thesis)
- GADT as a type class (or encode the type as it's fold):
class Exp e where
lit :: TyRange a = a - e a
plus :: e Int - e Int - e Int
and :: e Bool - e Bool - e Bool
- Notice we cannot construct an ill-typed expression, the Haskell
type-checker complains.
- |TyRange| is the class of indices:
class TyRange a
instance TyRange Int
instance TyRange Bool
- The behaviour is given by instances:
newtype Eval a = Eval {eval :: a}
instance Exp Eval where
lit = Eval
plus x y = Eval (eval x + eval y)
and x y = Eval (eval x eval y)
Extension is easy:
class Exp e = ExpIf e where
ifOp :: TyRange a = e Bool - e a - e a - e a
instance ExpIf Eval where
ifOp c t e = Eval (if (eval c) then (eval t) else (eval e))
class Exp e = ExpMult e where
mult :: e Int - e Int - e Int
instance ExpMult Eval where
mult x y = Eval (eval x * eval y)
- Adding new meta-level types is easy:
instance TyRange a = TyRange [a]
instance TyRange Char
class Exp e = ExpConcat e where
conc :: e [Char] - e [Char] - e [Char]
instance ExpConcat Eval where
conc x y = Eval (eval x ++ eval y)
- Closing expressions is also easy: wrap around a type and provide
new functions:
data TyRange a = Wrap a = Wrap (forall e. (Exp e, ExpIf e, ExpMult e,
ExpConcat e) = e a)
evalExp :: TyRange a = Wrap a - a
evalExp (Wrap x) = eval x
- Some expresions:
Compare:
exp1 :: Exp e = e Int
exp1 = plus (lit 3) (lit 3)
val1 = eval exp1
With:
exp1' :: Eval Int
exp1' = plus (lit 3) (lit 3)
va1' = eval exp1
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] A type signature inferred by GHCi that is rejected when written explicitly
I find this interesting,
GHCi accepts a function |dmap| which I show below and infers its type,
but if I annotate the function with the inferred type, GHCi's
type-checker rejects it.
I'm trying to generalise the datatype-generic dmap:
dmap :: Bifunctor s = (a - b) - Fix s a - Fix s b
dmap f = In . bimap (dmap f) f . out
where
data Fix s a = In { out :: s (Fix s a) a }
class Bifunctor s where
bimap :: (a - c) - (b - d) - s a b - s c d
The idea is that recursive types are represented by their
(lamba-lifted) functors, eg:
data ListF b a = NilF | ConsF a b
instance Bifunctor ListF where
bimap f g NilF = NilF
bimap f g (ConsF a b)= ConsF (g a) (f b)
I now define two classes:
class From a c x where
from :: a x - c x
class To a c y where
to :: c y - a y
And a generic |gmap| which given the map for |c| and a mapping for |x|
delivers the map for |a|:
type GMap t x y = (x - y) - t x - t y
gmap :: (From a c x, To a c y) = GMap c x y - GMap a x y
gmap gmc gmx = to . gmc gmx . from
I want to write |dmap| as a special case of |gmap|, but I can't even
get there. If I write
dmap f = to . bimap (dmap f) f . from
GHCi infers it has type (up to renaming):
(From a1 (s (a1 x)) x, Bifunctor s, To a2 (s (a2 y)) y) = (x - y)
- a1 x - a2 y
But if I cut and paste the type into the code I get type errors:
Could not deduce (From a1 (s1 (a11 x)) x) ...
Could not deduce (From a11 (s1 (a11 x)) x, To a21 (s1 (a21 y)) y) ...
Could not deduce (From a1 (s1 (a11 x)) x) ...
Interesting,
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANNOUNCE: Generic Haskell 1.80 (Emerald)
This has certainly been taken into account when comparing approaches to generic programming. I quote from page 18/19 from the work you and Bulat Indeed I was not aware of it. Missed that. Thanks for pointing it out! Thus, full reflexivity of an approach is taken into account. This suggests constrained types are part of Haskell98. So, I'm a bit confused at the moment as well. After reading the Haskell 98 report more carefully I think constrained types are part of Haskell98. The syntax for algebraic datatype declarations given is: data cx = T u1 ... uk = K1 t11 ... t1k1 | ...| Kn tn1 ... tnkn Certainly, they are implemented in a peculiar way, with constraints associated with value constructors and not the type, perhaps to keep the class and kinds orthogonal (eg, the BinTree type has * - * kind instead of Ord - * kind). At any rate, this has been discussed before in other threads. Thanks Thomas for your help P. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANNOUNCE: Generic Haskell 1.80 (Emerald)
On 12/04/2008, Thomas van Noort [EMAIL PROTECTED] wrote: Generic Haskell includes the following features: * type-indexed values -- generic functions that can be instantiated on all Haskell data types. ^^^ I have perused the manual and wonder if parametric types with class constraints are now supported or are not considered Haskell types. I'm thinking of types such as data Ord a = BinTree a = Leaf | Node a (BinTree a) (BinTree a) data Functor f = GRose f a = GLeaf | GNode a (f(GTree f a)) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANNOUNCE: Generic Haskell 1.80 (Emerald)
On 12/04/2008, Thomas van Noort [EMAIL PROTECTED] wrote: That's a good question. Unfortunately, only Haskell98 types are currently supported by the Generic Haskell compiler. I thought constrained types were Haskell 98, but now I'm in doubt... But at first sight, implementing support for parametric types with class constraints is not too hard. Class constraints of a parametric type need to be propagated to its generated structure type. Certainly, but there are a few difficulties for higher-kinded types. An arguable solution: http://portal.acm.org/citation.cfm?id=1159868 The reason I mention this is because Scrap your Boilerplate supports them whereas GH does not, and I'm not aware this has been taken into account when comparing these two approaches in the work cited by Bulat on this thread. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why is this strict in its arguments?
Hasn't Ryan raised an interesting point, though? Bottom is used to denote non-termination and run-time errors. Are they the same thing? To me, they're not. A non-terminating program has different behaviour from a failing program. When it comes to strictness, the concept is defined in a particular semantic context, typically an applicative structure: [[ f x ]] = App [[f]] [[x]] Function f is strict if App [[f]] _|_ = _|_ Yet, that definition is pinned down in a semantics where what _|_ models is clearly defined. I don't see why one could not provide a more detailed semantics where certain kinds of run-time errors are distinguished from bottom. Actually, this already happens. Type systems are there to capture many program properties statically. Some properties that can't be captured statically are captured dynamically: the compiler introduces run-time tests. Checking for non-termination is undecidable, but putting run-time checks for certain errors is not. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] foild function for expressions
I believe the exercise is about understanding folds. There are two references that are related to the exercise: A tutorial on the universality and expressiveness of fold, by Graham Hutton. Dealing with large bananas, by Ralf Lammel, etc. The last paper motivates well the need to gather all the function parameters to the fold (ie, the algebra) in a separate record structure. I don't think being told what to write will help you understand what is going on, which is simpler than it seems. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Rigid type-var unification failure in existentials used with parametrically polymorphic functions
Stupid of me: Isn't the code for mapBox :: forall a. (a - a) - Box - Box encoding the proof: Assume forall a. a - a Assume exists a.a unpack the existential, x :: a = T for some T apply f to x, we get (f x) :: a pack into existential, B (f x) :: exists a.a Discharge first assumption Discharge second assumption The error must be in step 3. Sorry if this is obvious, it's not to me right now. The proof outlined is that of (forall a. a - a) - Box - Box, my apologies. We have to prove a universally quantified formula and that requires forall-introduction. If someone has the proof in the tip of their fingers, I'm grateful if you could let me know. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Rigid type-var unification failure in existentials used with parametrically polymorphic functions
A question about existential quantification: Given the existential type: data Box = forall a. B a in other words: -- data Box = B (exists a.a) -- B :: (exists a.a) - Box I cannot type-check the function: mapBox :: forall a b. (a - b) - Box - Box --:: forall a b. (a - b) - (exists a.a) - (exists a.a) mapBox f (B x) = B (f x) Nor can I type check: mapBox :: forall a. (a - a) - Box - Box --:: forall a. (a - a) - (exists a.a) - (exists a.a) mapBox f (B x) = B (f x) The compiler tells me that in both functions, when it encounters the expression |B (f x)|, it cannot unify the universally quantified |a| (which generates a rigid type var) with the existentially quatified |a| (which generates a different rigid type var) -- or so I interpret the error message. However, at first sight |f| is polymorphic so it could be applied to any value, included the value hidden in |Box|. Of course, this works: mapBox :: (forall a b. a - b) - Box - Box mapBox f (B x) = B (f x) Because it's a tautology: given a proof of a - b for any a or b I can prove Box - Box. However the only value of type forall a b. a - b is bottom. This also type-checks: mapBox :: (forall a. a - a) - Box - Box mapBox f (B x) = B (f x) When trying to give an explanation about why one works and the other doesn't, I see that, logically, we have: forall a. P(a) = Q implies (forall a. P(a)) = Q when a does not occur in Q. The proof in our scenario is trivial: p :: (forall a. (a - a) - (Box - Box)) - (forall a. a - a) - Box - Box p mapBox f b = mapBox f b However, the converse is not true. Yet, could somebody tell me the logical reason for the type-checking error? In other words, how does the unification failure translate logically. Should the first mapBox actually type-check? Isn't the code for mapBox :: forall a. (a - a) - Box - Box encoding the proof: Assume forall a. a - a Assume exists a.a unpack the existential, x :: a = T for some T apply f to x, we get (f x) :: a pack into existential, B (f x) :: exists a.a Discharge first assumption Discharge second assumption The error must be in step 3. Sorry if this is obvious, it's not to me right now. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Rigid type-var unification failure in existentials used with parametrically polymorphic functions
mapBox :: forall a b. (a - b) - Box - Box --:: forall a b. (a - b) - (exists a.a) - (exists a.a) mapBox f (B x) = B (f x) However, at first sight |f| is polymorphic so it could be applied to any value, included the value hidden in |Box|. f is not polymorphic here; mapBox is. I see, it's a case of not paying proper attention. I presume this will reflect in the imposibility of introducing the forall when trying to prove the type. Yes, but that is only because your Box type is trivial. It can contain any value, so you can never extract any information from it. Indeed, I was just trying to play with unconstrained existentials. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Pierce on type theory and category theory
Another opinion in case you need more: TAPL is excellent for self-study. There are solutions for most interesting exercises. And every type system presented comes with a downloadable implementation. You can practice with it and change it. Do not hesitate to get it. I also recommend Cardelli's papers on types which are free to obtain. The Basic Category Theory book is, as the title says, basic. It is a sort of polished study notes (and I recall Pierce saying something along this line in the introduction). Several examples and exercises are taken from Goldblatt's Topoi, the Categorical Analysis of Logic, whose first chapters are a good starting point in Category theory but he introduces category-theoretic concepts from set-theoretic ones and it can be hard to abstract properly from one example. Pierce's book is well-written, introductory, there's nice stuff on cartesian closed categories and F-algebras, and the best thing is its excellent annotated bibliography which will help you to move on. Given its price and size, I think its worth. You'll need more stuff. There are books and tutorials out there. MacLane I guess is a must, if only for breadth and precision. There's Steve Awodey's book (Oxford University Press). I found Harold Simmon's notes Category Theory in four easy movements enjoyable and readable, especially the stuff on limits. Lawere's book mentioned by others is also fun. Fokkinga has an excellent introduction to category theory from a calculational standpoint, with notation and concepts used in the Bananas paper. There is also Barr and Wells's third edition. And of course, Mitchell's encyclopedic Foundations for Programming Languages. To conclude, there are loads of sources and for self study, I'd recommend to use several books and several tutorial notes, if only to contrast approaches, definitions, to have exercises and solutions, etc. And there's the wikipedia as well. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Lack of expressiveness in kinds?
On 16/03/07, [EMAIL PROTECTED] [EMAIL PROTECTED] wrote: There is a wide-spread opinion that one ought not to give context to a data type declaration (please search for `restricted datatypes Haskell'). Someone said that in GHC typechecker such contexts called stupidctx. There has been a proposal to remove that feature from Haskell, although I like it as a specification tool. John Hughes wrote a paper about a better use for that feature: I'd like to qualify this remark by adding that, to me, this opinion arises from the fact that compilers treat constraints as orthogonal to kinds, but not from the fact that constraints are a bad idea. I also want to point Andrew to the fact that constraints are not associated with the type but with (some of) the value constructors, perhaps in order to keep the kind system intact. For example, define data Eq a = Set a = MkSet [a] I'd say we need the constraint in order to define a set. Nevertheless, evaluate const 0 (undefined :: Set (Int - Int)) Funny we can give undefined the type Set (Int - Int) when functions have no Eq instance. Another example, define: data Eq a = Foo a = FNil | FCons a (Foo a) the type of the value constructors is : FNil :: Foo a FCons :: Eq a = a - Foo a - Foo a By not putting the constraint in the polymorphic value FNil we may get silly type errors when there are none. As I understand, ideally the constraint restricts the range of types to which the type constructor can be applied. Hardly a kind * - * then, for * stands for the whole universe of types (not type constructors). Passing the potato to the value system and letting the value constructors bring up the constraints in construction or pattern matching is not the same thing. Then we have the complaint that if we want to use a constrained type then we have to place constraints in all the functions that use it, so why not put them there. In other words, instead of data Ord a = BinTree a = Leaf | Node a (BinTree a) (BinTree a) insert :: Ord a = a - BinTree a - BinTree a let's write: data BinTree a = Leaf | Node a (BinTree a) (BinTree a) insert :: Ord a = a - BinTree a - BinTree a However, I find this wrong from a formal point of view. The constraint is associated with the type, not the functions. Compare with the list type and the function sort, which has an Ord constraint which belongs to the function. There is no such thing as a constrained list *type*, only that sort takes a list with elements in ord and no other list. From a practical point of view, if you like type inference, you may omit the constraint in the functions if it appears in one place, that is, where the type is defined. (To recall, John Hugues paper begins with the complaint that changing the constraint in the type affects the type signatures of functions when written explicitly.) The solution perhaps is not to ignore constraints and treat them as a minor evil, but to make them an integral part of the type system, as entities that can be passed as arguments and returned as results at the type level. And also as parameters to class declarations. A questionable implementation decision should not be the origin of a recommended style of programming. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Fwd: [Haskell-cafe] GADTs: the plot thickens?
-- Forwarded message -- From: Pablo Nogueira [EMAIL PROTECTED] Date: 31-Jan-2007 12:04 Subject: Re: [Haskell-cafe] GADTs: the plot thickens? To: Conor McBride [EMAIL PROTECTED] I haven't tried this yet, but would declaring the class Nat be a starting point? class Nat n instance Nat Z instance Nat n = Nat (S n) data Fin :: * - * where Fz :: Nat n = Fin (S n) Fs :: Nat n = Fin n - Fin (S n) thin :: Nat n = Fin (S n) - Fin n - Fin (S n) thicken :: Fin (S n) - Fin (S n) - Maybe (Fin n) Btw, apparently we have to use GHC HEAD if we want GADTs to compile properly. The error seems very similar to the one you get when trying to write (++) for dependent lists with length encoded as GADTs. To make sure I understand, you are asking if there is a hack that will enable us to tell the Haskell type checker that n = (S n1), right? Regards, P. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] GADTs: the plot thickens?
Bruno, Now we modify thin to take an extra Nat n (not needed, but just to show the duality with thickening): I'm puzzled by the not needed bit. Isn't the introduction of Fin's indices reflected as values in the GADT , and the fact that the GADT makes that reflection, what makes it work? P. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] GADTs: the plot thickens?
Aha, of course, Sorry, I misunderstood you. P. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
