Re: [Haskell-cafe] Church vs Boehm-Berarducci encoding of Lists
do you have any references for the extension of lambda-encoding of data into dependently typed systems? Is there a way out of this quagmire? Or are we stuck defining actual datatypes if we want dependent types? Although not directly answering your question, the following paper Inductive Data Types: Well-ordering Types Revisited Healfdene Goguen Zhaohui Luo http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.17.8970rep=rep1type=pdf might still be relevant. Sec 2 reviews the major approaches to inductive data types in Type Theory. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Haskell Wiki News
This doesn't seem to be up-to-date. It announces GHC 7.4 released (but 7.6.1 was released a couple of weeks ago). ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Question about type inference of a GADT term
-BEGIN PGP SIGNED MESSAGE-
Hash: SHA1
Yes, of course! Stupid me, thanks for pointing that out Daniel.
Now it works as expected.
Florian
On 09/22/2012 12:55 AM, Daniel Peebles wrote:
Shouldn't you have
IxZero :: Ix (CtxCons ty ctx) ty
instead of
IxZero :: Ix ctx ty
On Fri, Sep 21, 2012 at 8:34 AM, Florian Lorenzen
florian.loren...@tu-berlin.de
mailto:florian.loren...@tu-berlin.de wrote:
Hello cafe,
I have the following GADT definitions capturing the simply typed
lambda calculus with de Bruijn indices for variables and
explicitly annotated types for variables:
{-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE
DataKinds #-}
-- Typing contexts data Ctx = CtxNil | CtxCons Ctx Type
-- Types data Type = TyInt | TyArrow Type Type
-- Variable indices data Ix (ctx :: Ctx) (ty :: Type) where IxZero
:: Ix ctx ty IxSucc :: Ix ctx ty1 - Ix (CtxCons ctx ty2) ty1
-- Type representations data TyRep (ty :: Type) where TyRepInt ::
TyRep TyInt TyRepArrow :: TyRep ty1 - TyRep ty2 - TyRep (TyArrow
ty1 ty2)
-- Terms data Term (ctx :: Ctx) (ty :: Type) where TmInt :: Integer
- Term ctx TyInt TmVar :: Ix ctx ty - Term ctx ty TmAdd :: Term
ctx TyInt - Term ctx TyInt - Term ctx TyInt TmApp :: Term ctx
(TyArrow ty1 ty2) - Term ctx ty1 - Term ctx ty2 TmAbs :: TyRep
ty1 - Term (CtxCons ctx ty1) ty2 - Term ctx (TyArrow ty1 ty2)
For the following definition
test1 = TmAbs TyRepInt (TmVar IxZero)
GHCi infers the type
test1 :: Term ctx (TyArrow 'TyInt ty2)
I was a bit puzzled because I expected
Term ctx (TyArrow TyInt TyInt)
Of course, this more special type is an instance of the inferred
one, so I can assign it by a type signature.
Can someone explain why the inferred type is more general?
Terms like
test2 = TmAbs TyRepInt (TmAdd (TmVar IxZero) (TmInt 5))
have the type I expected:
test2 :: Term ctx (TyArrow 'TyInt 'TyInt)
Thank you and best regards,
Florian
___ Haskell-Cafe
mailing list Haskell-Cafe@haskell.org
mailto:Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
- --
Florian Lorenzen
Technische Universität Berlin
Fakultät IV - Elektrotechnik und Informatik
Übersetzerbau und Programmiersprachen
Sekr. TEL12-2, Ernst-Reuter-Platz 7, D-10587 Berlin
Tel.: +49 (30) 314-24618
E-Mail: florian.loren...@tu-berlin.de
WWW:http://www.user.tu-berlin.de/florenz/
-BEGIN PGP SIGNATURE-
Version: GnuPG v1.4.11 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://www.enigmail.net/
iEYEARECAAYFAlBdktYACgkQvjzICpVvX7ZskwCgnJC9VaIkoWHuTZoP8kGg70Tb
MFsAn0yuBDClSxe32ZTO8pZzz1xOpI2T
=EoV6
-END PGP SIGNATURE-
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Munich Haskell Meeting
Dear all, Heinrich is on holiday next week, thus I'll manage it this time: Once again, it's time for our monthly get-together. Functional programmers from Munich and other cities will meet on Thu, 27th of September, at 19h30 at Cafe Puck in Munich. If you plan to join, please go to http://www.haskell-munich.de/dates and click the button! With hope to meet many of you there, -- Christian Neukirchen chneukirc...@gmail.com http://chneukirchen.org ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell Wiki News
It's a wiki. I went ahead and fixed it, this time. To paraphrase Bryan O'Sullivan: Whenever you think why hasn't anyone done ..., or why doesn't somebody fix ..., you should ask yourself Why don't *I* do ... or Why don't *I* fix That's how open source works. (Not trying to be offensive, just pointing out that's how we should think about open source. That's how we got Real World Haskell, that's how we got Criterion, that's how we got the text package in its current version.) On 22 September 2012 10:40, Colin Adams colinpaulad...@gmail.com wrote: This doesn't seem to be up-to-date. It announces GHC 7.4 released (but 7.6.1 was released a couple of weeks ago). ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- Push the envelope. Watch it bend. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Fwd: ANNOUNCE: hsqml-0.1.1 (and hsqml-morris-0.1.0)
Hello, In case anyone is wondering this does not compile on vanilla Mac OS 10.6 because XCode 3.2 doesn't support C++11. I believe that XCode 4.2 does support it however I've not yet paid Apple the $100 they want before I can download it for 10.6. Macports has more recent versions of GCC however this option turned out to be fraught with difficulties[1][2]. Has anybody got HsQML working with XCode 4.2? Matt [1] https://trac.macports.org/wiki/UsingTheRightCompiler [2] http://www.haskell.org/haskellwiki/Mac_OS_X_Strike_Force On 11 Sep 2012, at 08:47, Robin KAY wrote: Dear All, I would like to announce a new package called 'hsqml' [1]. HsQML provides a Haskell binding to the Qt Quick framework. It allows you to write graphical applications where the front-end is written in Qt Quick's QML language (incorporating JavaScript) and the back-end is written in Haskell. The two layers are coupled together via a facility to define custom JavaScript objects through which QML code can call into Haskell. HsQML requires an installation of Qt 4.7 (including QtDeclarative) or later on your path. It has been tested with GHC 7.4 on both Linux and Windows. There is also a simple example program available using HsQML on Hackage called 'hsqml-morris'. It implements a human v computer game of Nine Men's Morris with game logic and AI written in Haskell and the presentation layer in QML. The library is currently limited by a lack of support for Qt signals, so calls can only be made from JavaScript to Haskell and not the other way. I plan to add support for these in a future release. Migration over to Qt 5.x is also likely once it's released. [1] http://hackage.haskell.org/package/hsqml-0.1.1 [2] http://hackage.haskell.org/package/hsqml-morris-0.1.0 Regards, -- Robin KAY ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Darcs on Windows 7
Hello Haskellers, I installed darcs on a Windows 7 machine. A darcs folder was created under Program Files(x86) folder. However, when I pull up Program... on the left side, darcs not there for me to run it. Why? Is darcs run only from the CLI? Regard, Vasili ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Darcs on Windows 7
Vasili I. Galchin wrote: Hello Haskellers, I installed darcs on a Windows 7 machine. A darcs folder was created under Program Files(x86) folder. However, when I pull up Program... on the left side, darcs not there for me to run it. Why? Is darcs run only from the CLI? Yes, darcs is a command line program. Erik -- -- Erik de Castro Lopo http://www.mega-nerd.com/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Call for discussion: OverloadedLists extension
(Prettier formatting available at: https://gist.github.com/3761252) Many of us use the OverloadedStrings language extension on a regular basis. It provides the ability to keep the ease-of-use of string literal syntax, while getting the performance and correctness advantages of specialized datatypes like ByteString and Text. I think we can get the same kind of benefit by allowing another literal syntax to be overloaded, namely lists. ## Overly simple approach The simplest example I can think of is allowing easier usage of Vector: [1, 2, 3] :: Vector Int In order to allow this, we could use a typeclass approach similar to how OverloadedStrings works: class IsList a where fromList :: [b] - a b instance IsList Vector where fromList = V.fromList foo :: Vector Int foo = fromList [1, 2, 3] ## Flaws However, such a proposal does not allow for constraints, e.g.: instance IsList Set where fromList = Set.fromList No instance for (Ord b) arising from a use of `Set.fromList' In the expression: Set.fromList In an equation for `fromList': fromList = Set.fromList In the instance declaration for `IsList Set' Additionally, it provides for no means of creating instances for datatypes like Map, where the contained value is not identical to the value contained in the original list. In other words, what I'd like to see is: [(foo, 1), (bar, 2)] :: Map Text Int ## A little better: MPTC A simplistic approach to solve this would be to just use MultiParamTypeClasses: class IsList input output where fromList :: [input] - output instance IsList a (Vector a) where fromList = V.fromList foo :: Vector Int foo = fromList [1, 2, 3] Unfortunately, this will fail due to too much polymorphism: No instance for (IsList input0 (Vector Int)) arising from a use of `fromList' Possible fix: add an instance declaration for (IsList input0 (Vector Int)) In the expression: fromList [1, 2, 3] In an equation for `foo': foo = fromList [1, 2, 3] This can be worked around by giving an explicit type signature on the numbers in the list, but that's not a robust solution. In order to solve this properly, I think we need either functional dependencies or type families: ## Functional dependencies class IsList input output | output - input where fromList :: [input] - output instance IsList a (Vector a) where fromList = V.fromList instance Ord a = IsList a (Set a) where fromList = Set.fromList instance Ord k = IsList (k, v) (Map k v) where fromList = Map.fromList foo :: Vector Int foo = fromList [1, 2, 3] bar :: Set Int bar = fromList [1, 2, 3] baz :: Map String Int baz = fromList [(foo, 1), (bar, 2)] ## Type families class IsList a where type IsListInput a fromList :: [IsListInput a] - a instance IsList (Vector a) where type IsListInput (Vector a) = a fromList = V.fromList instance Ord a = IsList (Set a) where type IsListInput (Set a) = a fromList = Set.fromList instance Ord k = IsList (Map k v) where type IsListInput (Map k v) = (k, v) fromList = Map.fromList foo :: Vector Int foo = fromList [1, 2, 3] bar :: Set Int bar = fromList [1, 2, 3] baz :: Map String Int baz = fromList [(foo, 1), (bar, 2)] ## Conclusion Consider most of this proposal to be a strawman: names and techniques are completely up to debate. I'm fairly certain that our only two choices to implement this extension is a useful way is fundeps and type families, but perhaps there's another approach I'm missing. I don't have any particular recommendation here, except to say that fundeps is likely more well supported by other compilers. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
