Re: [Haskell-cafe] Type checking the content of a string
Up on that, anybody already tried to load an haskell interpreter in a
QuasiQuoter?
On Sat, Feb 23, 2013 at 12:03 AM, Corentin Dupont corentin.dup...@gmail.com
wrote:
I'm trying to load my interpreter in the Q monad:
cr :: QuasiQuoter
cr = QuasiQuoter { quoteExp = quoteRuleFunc}
quoteRuleFunc :: String - Q TH.Exp
quoteRuleFunc s = do
res - runIO $ runInterpreter $ do
setImports [Prelude, Language.Nomyx.Rule,
Language.Nomyx.Expression, Language.Nomyx.Test,
Language.Nomyx.Examples, GHC.Base, Data.Maybe]
interpret s (as :: RuleFunc)
case res of
Right _ - [| s |]
Left e - fail $ show e
However, I always obtain an error durring compilation:
...
Loading package XXX ... linking ... done.
GHCi runtime linker: fatal error: I found a duplicate definition for symbol
__stginit_ghczm7zi4zi1_DsMeta
whilst processing object file
/usr/lib/ghc/ghc-7.4.1/libHSghc-7.4.1.a
This could be caused by:
* Loading two different object files which export the same symbol
* Specifying the same object file twice on the GHCi command line
* An incorrect `package.conf' entry, causing some object to be
loaded twice.
GHCi cannot safely continue in this situation. Exiting now. Sorry.
I vaguely understand that the interpreted modules are conflicting with the
compiled ones...
On Fri, Feb 22, 2013 at 11:51 PM, Corentin Dupont
corentin.dup...@gmail.com wrote:
Great! That seems very powerful. So you can do what you want during
compilation, readin files, send data over the network?
Other question, in my example how can I halt the compilation if a test
program is wrong?
On Fri, Feb 22, 2013 at 8:30 PM, Francesco Mazzoli f...@mazzo.li wrote:
At Fri, 22 Feb 2013 19:43:51 +0100,
Corentin Dupont wrote:
Hi Adam,
that looks interresting. I'm totally new to TH and QuasiQuotes, though.
Can I run IO in a QuasiQuoter? I can run my own interpreter.
Yes, you can:
http://hackage.haskell.org/packages/archive/template-haskell/2.8.0.0/doc/html/Language-Haskell-TH.html#v:runIO
.
Francesco
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type checking the content of a string
On Fri, Feb 22, 2013 at 06:44:06PM +0100, Corentin Dupont wrote: Hi all, I have a program able to read another program as a string, and interpret it (using Hint). I'd like to make unit tests, so I have a file Test.hs containing a serie of test programs as strings. However, how could I be sure that these test program are syntactically valid, at compile time? If you just want to check whether a program is syntactically valid, you can use the haskell-src-exts package to parse it. If you also want to do some type checking you can try the haskell-type-exts package. -Brent ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type checking the content of a string
Finally, I solved the problem using typeOf instead of interpret:
cr :: QuasiQuoter
cr = QuasiQuoter { quoteExp = quoteRuleFunc}
quoteRuleFunc :: String - Q TH.Exp
quoteRuleFunc s = do
res - runIO $ runInterpreter $ do
setImports [Prelude, Language.Nomyx.Expression]
typeOf s
case res of
Right RuleFunc - [| s |]
Right _ - fail $ Rule doesn't typecheck
Left e - fail $ show e
I don't know really why, but now it's working very well!
On Sat, Feb 23, 2013 at 7:56 PM, Daniel Gorín jcpetru...@gmail.com wrote:
Hi Corentin,
I've never used TH, but from what I understand, trying to combine hint and
TH would be redundant (even if it worked): whatever String you can evaluate
using hint, you can evaluate it directly in TH. Is this not the case?
Cheers,
Daniel
On Feb 23, 2013, at 6:53 PM, Corentin Dupont wrote:
Hi Daniel,
Did you already tried to use Hint in a QuasiQuote? This would come handy
to check at compile time the validity of some strings...
However I have the error hereunder.
The duplicate symbol found in the object file is in fact the first
symbol in this file. So I guess GHCi tries to load it twice...
Best,
Corentin
On Sat, Feb 23, 2013 at 12:03 AM, Corentin Dupont
corentin.dup...@gmail.com wrote:
I'm trying to load my interpreter in the Q monad:
cr :: QuasiQuoter
cr = QuasiQuoter { quoteExp = quoteRuleFunc}
quoteRuleFunc :: String - Q TH.Exp
quoteRuleFunc s = do
res - runIO $ runInterpreter $ do
setImports [Prelude, Language.Nomyx.Rule,
Language.Nomyx.Expression, Language.Nomyx.Test,
Language.Nomyx.Examples, GHC.Base, Data.Maybe]
interpret s (as :: RuleFunc)
case res of
Right _ - [| s |]
Left e - fail $ show e
However, I always obtain an error during compilation:
...
Loading package XXX ... linking ... done.
GHCi runtime linker: fatal error: I found a duplicate definition for
symbol
__stginit_ghczm7zi4zi1_DsMeta
whilst processing object file
/usr/lib/ghc/ghc-7.4.1/libHSghc-7.4.1.a
This could be caused by:
* Loading two different object files which export the same symbol
* Specifying the same object file twice on the GHCi command line
* An incorrect `package.conf' entry, causing some object to be
loaded twice.
GHCi cannot safely continue in this situation. Exiting now. Sorry.
I vaguely understand that the interpreted modules are conflicting with
the compiled ones...
On Fri, Feb 22, 2013 at 11:51 PM, Corentin Dupont
corentin.dup...@gmail.com wrote:
Great! That seems very powerful. So you can do what you want during
compilation, readin files, send data over the network?
Other question, in my example how can I halt the compilation if a test
program is wrong?
On Fri, Feb 22, 2013 at 8:30 PM, Francesco Mazzoli f...@mazzo.li wrote:
At Fri, 22 Feb 2013 19:43:51 +0100,
Corentin Dupont wrote:
Hi Adam,
that looks interresting. I'm totally new to TH and QuasiQuotes, though.
Can I run IO in a QuasiQuoter? I can run my own interpreter.
Yes, you can:
http://hackage.haskell.org/packages/archive/template-haskell/2.8.0.0/doc/html/Language-Haskell-TH.html#v:runIO
.
Francesco
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Type checking the content of a string
Hi all, I have a program able to read another program as a string, and interpret it (using Hint). I'd like to make unit tests, so I have a file Test.hs containing a serie of test programs as strings. However, how could I be sure that these test program are syntactically valid, at compile time? Those programs should have the type RuleFunc. I tried some TH: printProg :: Q Exp - String printProg p = unsafePerformIO $ do expr - runQ p return $ pprint expr myTest = printProg [| my test program :: RuleFunc |] But it's not very satisfatory yet. When pretty printing TH changes the program quite a bit and my interpreter cannot compile it due to scoping problems. I'd like to have my test program copied back as is. Is it possible? Any other solutions? Thanks a lot! Corentin ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type checking the content of a string
On Fri, Feb 22, 2013 at 12:44 PM, Corentin Dupont corentin.dup...@gmail.com wrote: Hi all, I have a program able to read another program as a string, and interpret it (using Hint). I'd like to make unit tests, so I have a file Test.hs containing a serie of test programs as strings. However, how could I be sure that these test program are syntactically valid, at compile time? Hi Corentin, You could write the test programs like: test1 :: String test1 = [qq| x+1 == 3 |] Where qq is a QuasiQuoter you have to define. It could try to parse the string with http://hackage.haskell.org/package/haskell-src-exts, and if that succeeds, returns the original string. -- Adam ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type checking the content of a string
Hi Adam, that looks interresting. I'm totally new to TH and QuasiQuotes, though. Can I run IO in a QuasiQuoter? I can run my own interpreter. On Fri, Feb 22, 2013 at 7:12 PM, adam vogt vogt.a...@gmail.com wrote: On Fri, Feb 22, 2013 at 12:44 PM, Corentin Dupont corentin.dup...@gmail.com wrote: Hi all, I have a program able to read another program as a string, and interpret it (using Hint). I'd like to make unit tests, so I have a file Test.hs containing a serie of test programs as strings. However, how could I be sure that these test program are syntactically valid, at compile time? Hi Corentin, You could write the test programs like: test1 :: String test1 = [qq| x+1 == 3 |] Where qq is a QuasiQuoter you have to define. It could try to parse the string with http://hackage.haskell.org/package/haskell-src-exts, and if that succeeds, returns the original string. -- Adam ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type checking the content of a string
At Fri, 22 Feb 2013 19:43:51 +0100, Corentin Dupont wrote: Hi Adam, that looks interresting. I'm totally new to TH and QuasiQuotes, though. Can I run IO in a QuasiQuoter? I can run my own interpreter. Yes, you can: http://hackage.haskell.org/packages/archive/template-haskell/2.8.0.0/doc/html/Language-Haskell-TH.html#v:runIO. Francesco ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type checking the content of a string
Great! That seems very powerful. So you can do what you want during compilation, readin files, send data over the network? Other question, in my example how can I halt the compilation if a test program is wrong? On Fri, Feb 22, 2013 at 8:30 PM, Francesco Mazzoli f...@mazzo.li wrote: At Fri, 22 Feb 2013 19:43:51 +0100, Corentin Dupont wrote: Hi Adam, that looks interresting. I'm totally new to TH and QuasiQuotes, though. Can I run IO in a QuasiQuoter? I can run my own interpreter. Yes, you can: http://hackage.haskell.org/packages/archive/template-haskell/2.8.0.0/doc/html/Language-Haskell-TH.html#v:runIO . Francesco ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type checking the content of a string
I'm trying to load my interpreter in the Q monad:
cr :: QuasiQuoter
cr = QuasiQuoter { quoteExp = quoteRuleFunc}
quoteRuleFunc :: String - Q TH.Exp
quoteRuleFunc s = do
res - runIO $ runInterpreter $ do
setImports [Prelude, Language.Nomyx.Rule,
Language.Nomyx.Expression, Language.Nomyx.Test,
Language.Nomyx.Examples, GHC.Base, Data.Maybe]
interpret s (as :: RuleFunc)
case res of
Right _ - [| s |]
Left e - fail $ show e
However, I always obtain an error durring compilation:
...
Loading package XXX ... linking ... done.
GHCi runtime linker: fatal error: I found a duplicate definition for symbol
__stginit_ghczm7zi4zi1_DsMeta
whilst processing object file
/usr/lib/ghc/ghc-7.4.1/libHSghc-7.4.1.a
This could be caused by:
* Loading two different object files which export the same symbol
* Specifying the same object file twice on the GHCi command line
* An incorrect `package.conf' entry, causing some object to be
loaded twice.
GHCi cannot safely continue in this situation. Exiting now. Sorry.
I vaguely understand that the interpreted modules are conflicting with the
compiled ones...
On Fri, Feb 22, 2013 at 11:51 PM, Corentin Dupont corentin.dup...@gmail.com
wrote:
Great! That seems very powerful. So you can do what you want during
compilation, readin files, send data over the network?
Other question, in my example how can I halt the compilation if a test
program is wrong?
On Fri, Feb 22, 2013 at 8:30 PM, Francesco Mazzoli f...@mazzo.li wrote:
At Fri, 22 Feb 2013 19:43:51 +0100,
Corentin Dupont wrote:
Hi Adam,
that looks interresting. I'm totally new to TH and QuasiQuotes, though.
Can I run IO in a QuasiQuoter? I can run my own interpreter.
Yes, you can:
http://hackage.haskell.org/packages/archive/template-haskell/2.8.0.0/doc/html/Language-Haskell-TH.html#v:runIO
.
Francesco
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Haskell V Java type checking
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 checking over the Java type checking? 3) Are there more general advantages of Haskell type checking over Java type checking?Regards,Pat Haskell program===data Cdata Dclass A t whereinstance A C whereinstance A D whereclass A t = B t whereinstance B C whereinstance B D where=Java Program===import java.lang.Class;interface AT {}class A_INSTANCET implements AT {}interface BT extends AT{}class B_INSTANCET implements BT {}class C {}class D {}public class DEMO1 {public static void main(String args[]) {A_INSTANCEC ac = new A_INSTANCEC();A_INSTANCED ad = new A_INSTANCED();B_INSTANCEC bc = new B_INSTANCEC();B_INSTANCED bd = new B_INSTANCED();System.out.println(Object's Class name =+ ac.getClass().getName());System.out.println(Object's Class name =+ ad.getClass().getName());System.out.println(Object's Class name =+ bc.getClass().getName());System.out.println(Object's Class name =+ bd.getClass().getName()); }}
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type checking oddity -- maybe my own confusion
Ryan Newton wrote: The desired goal was that everywhere I construct a value using the Assign constructor, that the resulting value's type to be tainted by the AssignCap constraint. Your code essentially accomplishes the goal: data E m where Assign :: AssignCap m = V - E m - E m - E m Varref :: V - E m -- ... Every time you construct the value of the type (E m) with the Assign constructor, you have to constructively prove -- provide evidence for -- that the type m is a member of AssignCap. That evidence is stored within the E m value and so can be reused whenever it is needed later. Let us modify the example slightly: class AssignCap m class MutateCap m data E m where Assign :: AssignCap m = V - E m - E m - E m Mutate :: MutateCap m = V - E m - E m - E m Varref :: V - E m -- ... type V = String -- test1 :: E t - E t test1 (Assign v x1 x2) = Assign v x1 x2 -- test2 :: MutateCap t = E t - E t test2 (Assign v x1 x2) = Mutate v x1 x2 To use the constructor Assign, we need the evidence that AssignCap m holds. The deconstructed value (Assign v x1 x2) provides such an evidence (as a `hidden' field of the data type). Therefore, the inferred type for test1 has no constraints. In contrast, in test2 nothing provides Mutate with the evidence that MutateCap m holds. Therefore, the inferred type has the MutateCap m constraint. If storing the evidence is not desired, then one should use ordinary ADT with smart constructors: -- Data constructors should not be exported data E1 m = Assign1 V (E1 m) (E1 m) | Varref1 V isAssign (Assign1 v x1 x2) = Just (v,x1,x2) isAssign _ = Nothing assign :: AssignCap m = V - E1 m - E1 m - E1 m assign = Assign1 -- test3 :: AssignCap m = E1 m - E1 m test3 e | Just (v,x1,x2) - isAssign e = assign v x1 x2 OCaml has a so-called private constructors, which permit deconstruction but prohibit construction. They are quite handy, saving us trouble writing the views like isAssign. Actually... to go a bit further, I thought there was some way to arrange this so that, upon GHC type-checking the case statement, it would realize that certain cases are forbidden based on the type, and would consider the pattern match complete without them (or issue an error if they are present). The key word in the phrase ``certain cases are forbidden based on the type'' is _type_ -- rather than a type class. If you wish to use this special GADT feature, you have to `invert' your design. Rather than specifying what is _required_ to construct an (E m) value, you should specify what is _provided_. data E2 m where Assign2 :: V - E2 m - E2 m - E2 IOT Varref2 :: V - E2 PureT test4 :: E2 IOT - E2 IOT test4 (Assign2 v x1 x2) = Assign2 v x1 x2 test4 (Varref2 _) = undefined The compiler complaints Couldn't match type `IOT' with `PureT' Inaccessible code in a pattern with constructor Varref2 :: V - E2 PureT, in an equation for `test4' In the pattern: Varref2 _ In an equation for `test4': test4 (Varref2 _) = undefined as desired. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Type checking oddity -- maybe my own confusion
Hi all,
Is there something wrong with the code below? My anticipation was that the
type of test would include the class constraint, because it uses the
Assign constructor. But if you load this code in GHCI you can see that the
inferred type was test :: E m - E m.
Thanks,
-Ryan
{-# LANGUAGE GADTs #-}
class AssignCap m
data PureT
data IOT
instance AssignCap IOT
data E m where
Assign :: AssignCap m = V - E m - E m - E m
Varref :: V - E m
-- ...
type V = String
-- I expected the following type but am not getting it:
-- test :: AssignCap m = E m - E m
test x =
case x of
Assign v e1 e2 - Assign v e1 e2
-- And this is the same:
Assign v e1 e2 - x
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type checking oddity -- maybe my own confusion
Hi Ryan,
Think of AssignCap as an extra argument packaged up with the Assign
constructor. When
you pattern match against Assign you make the AssignCap constraint *available*
for use in
the RHS of the pattern; so there's no need for quantification, you already have
the constraint
you want packaged inside your argument. (Back in the old times when GHC did not
implement
implication constraints maybe you'd get the type you say). Does that help?
Thanks
d-
From: haskell-cafe-boun...@haskell.org
[mailto:haskell-cafe-boun...@haskell.org] On Behalf Of Ryan Newton
Sent: 12 July 2011 16:02
To: Haskell Cafe
Subject: [Haskell-cafe] Type checking oddity -- maybe my own confusion
Hi all,
Is there something wrong with the code below? My anticipation was that the
type of test would include the class constraint, because it uses the Assign
constructor. But if you load this code in GHCI you can see that the inferred
type was test :: E m - E m.
Thanks,
-Ryan
{-# LANGUAGE GADTs #-}
class AssignCap m
data PureT
data IOT
instance AssignCap IOT
data E m where
Assign :: AssignCap m = V - E m - E m - E m
Varref :: V - E m
-- ...
type V = String
-- I expected the following type but am not getting it:
-- test :: AssignCap m = E m - E m
test x =
case x of
Assign v e1 e2 - Assign v e1 e2
-- And this is the same:
Assign v e1 e2 - x
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type checking oddity -- maybe my own confusion
On 07/12/2011 05:01 PM, Ryan Newton wrote:
Hi all,
Is there something wrong with the code below? My anticipation was that
the type of test would include the class constraint, because it uses
the Assign constructor. But if you load this code in GHCI you can see
that the inferred type was test :: E m - E m.
When I complete the pattern match in 'test', it might look like this:
test x = case x of
Assign v e1 e2 - x
Varref v - x
(which is just id :: E m - E m). Of course, we want to be able to write
test (Varref v)
for any v :: V, and match the second case. But as 'Varref' does not add
an AssignCap constraint, 'test' must not either.
Hope that helps. Steffen
Thanks,
-Ryan
{-# LANGUAGE GADTs #-}
class AssignCap m
data PureT
data IOT
instance AssignCap IOT
data E m where
Assign :: AssignCap m = V - E m - E m - E m
Varref :: V - E m
-- ...
type V = String
-- I expected the following type but am not getting it:
-- test :: AssignCap m = E m - E m
test x =
case x of
Assign v e1 e2 - Assign v e1 e2
-- And this is the same:
Assign v e1 e2 - x
___
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] Type checking oddity -- maybe my own confusion
Thanks, that does help. Very clear description.
Any good ideas about how to tweak my example to do what was intended ;-)?
The desired goal was that everywhere I construct a value using the Assign
constructor, that the resulting value's type to be tainted by the AssignCap
constraint.
Actually... to go a bit further, I thought there was some way to arrange
this so that, upon GHC type-checking the case statement, it would realize
that certain cases are forbidden based on the type, and would consider the
pattern match complete without them (or issue an error if they are present).
Thanks,
-Ryan
On Tue, Jul 12, 2011 at 11:17 AM, Dimitrios Vytiniotis
dimit...@microsoft.com wrote:
Hi Ryan,
** **
Think of AssignCap as an extra argument packaged up with the Assign
constructor. When
you pattern match against Assign you make the AssignCap constraint **
available** for use in
the RHS of the pattern; so there’s no need for quantification, you already
have the constraint
you want packaged inside your argument. (Back in the old times when GHC did
not implement
implication constraints maybe you’d get the type you say). Does that help?
** **
Thanks
d-
** **
** **
*From:* haskell-cafe-boun...@haskell.org [mailto:
haskell-cafe-boun...@haskell.org] *On Behalf Of *Ryan Newton
*Sent:* 12 July 2011 16:02
*To:* Haskell Cafe
*Subject:* [Haskell-cafe] Type checking oddity -- maybe my own confusion**
**
** **
Hi all,
** **
Is there something wrong with the code below? My anticipation was that the
type of test would include the class constraint, because it uses the
Assign constructor. But if you load this code in GHCI you can see that the
inferred type was test :: E m - E m.
** **
Thanks,
-Ryan
** **
** **
{-# LANGUAGE GADTs #-}
** **
class AssignCap m
data PureT
data IOT
instance AssignCap IOT
** **
data E m where
Assign :: AssignCap m = V - E m - E m - E m
Varref :: V - E m
-- ...
** **
type V = String
** **
-- I expected the following type but am not getting it:
-- test :: AssignCap m = E m - E m
test x =
case x of
Assign v e1 e2 - Assign v e1 e2
-- And this is the same:
Assign v e1 e2 - x
** **
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Manual Type-Checking to provide Read instances for GADTs. (was Re: [Haskell-cafe] Read instance for GATD)
That's really nice. Very interesting. Thank you.
On Fri, Jun 25, 2010 at 9:55 PM, Edward Kmett ekm...@gmail.com wrote:
I've obtained permission to repost Gershom's slides on how to deserialize
GADTs by typechecking them yourself, which are actually a literate haskell
source file, that he was rendering to slides. Consequently, I've just pasted
the content below as a literate email.
-Edward Kmett
-
Deserializing strongly typed values
(four easy pieces about typechecking)
Gershom Bazerman
-
prior art:
Oleg (of course)
http://okmij.org/ftp/tagless-final/course/course.html
...but also
Stephanie Weirich
http://www.comlab.ox.ac.uk/projects/gip/school/tc.hs
=
Ahem...
\begin{code}
{-# LANGUAGE DeriveDataTypeable,
ExistentialQuantification,
FlexibleContexts,
FlexibleInstances,
FunctionalDependencies,
GADTs,
RankNTypes,
ScopedTypeVariables
#-}
\end{code}
=
ahem.
\begin{code}
import Data.Typeable
import Data.Maybe
import Control.Monad.Error
import Control.Applicative
import qualified Data.Map as M
import Unsafe.Coerce
\end{code}
=
A simple ADT.
\begin{code}
data SimpleExpr = SOpBi String SimpleExpr SimpleExpr
| SOpUn String SimpleExpr
| SDbl Double
| SBool Bool deriving (Read, Show, Typeable)
\end{code}
Yawn.
=
An awesome GADT!
\begin{code}
data Expr a where
EDbl :: Double - Expr Double
EBool :: Bool - Expr Bool
EBoolOpBi :: BoolOpBi - Expr Bool - Expr Bool - Expr Bool
ENumOpBi :: NumOpBi - Expr Double - Expr Double - Expr Double
ENumOpUn :: NumOpUn - Expr Double - Expr Double
deriving Typeable
data NumOpBi = Add | Sub deriving (Eq, Show)
data NumOpUn = Log | Exp deriving (Eq, Show)
data BoolOpBi = And | Or deriving (Eq, Show)
\end{code}
The GADT is well typed. It cannot go wrong.
-
It also cannot derive show.
=
But we can write show...
\begin{code}
showIt :: Expr a - String
showIt (EDbl d) = show d
showIt (EBool b) = show b
showIt (EBoolOpBi op x y) = ( ++ show op
++ ++ showIt x
++ ++ showIt y ++ )
showIt (ENumOpBi op x y) = ( ++ show op
++ ++ showIt x
++ ++ showIt y ++ )
showIt (ENumOpUn op x) = show op ++ ( ++ showIt x ++ )
\end{code}
=
And eval is *much nicer*.
It cannot go wrong -- no runtime typechecks.
\begin{code}
evalIt :: Expr a - a
evalIt (EDbl x) = x
evalIt (EBool x) = x
evalIt (EBoolOpBi op expr1 expr2)
| op == And = evalIt expr1 evalIt expr2
| op == Or = evalIt expr2 || evalIt expr2
evalIt (ENumOpBi op expr1 expr2)
| op == Add = evalIt expr1 + evalIt expr2
| op == Sub = evalIt expr1 - evalIt expr2
\end{code}
=
But how do we write read!?
read EBool False = Expr Bool
read EDbl 12 = Expr Double
The type being read depends on the content of the string.
Even worse, we want to read not from a string that looks obvious
to Haskell (i.e. a standard showlike instance) but from
something that looks pretty to the user -- we want to *parse*.
So we parse into our simple ADT.
Then we turn our simple ADT into our nice GADT.
-
But how?
How do we go from untyped... to typed?
[And in general -- not just into an arbitrary GADT,
but an arbitrary inhabitant of a typeclass.]
[i.e. tagless final, etc]
=
Take 1:
Even if we do not know what type we are creating,
we eventually will do something with it.
So we paramaterize our typechecking function over
an arbitrary continuation.
\begin{code}
mkExpr :: (forall a. (Show a, Typeable a) = Expr a - r) - SimpleExpr -
r
mkExpr k expr = case expr of
SDbl d - k $ EDbl d
SBool b - k $ EBool b
SOpUn op expr1 - case op of
log - k $ mkExpr' (ENumOpUn Log) expr1
exp - k $ mkExpr' (ENumOpUn Exp) expr1
_ - error bad unary op
SOpBi op expr1 expr2 - case op of
add - k $ mkExprBi (ENumOpBi Add) expr1 expr2
sub - k $ mkExprBi (ENumOpBi Sub) expr1 expr2
\end{code}
=
Where's the typechecking?
\begin{code}
mkExpr' k expr = mkExpr (appCast $ k) expr
mkExprBi k expr1 expr2 = mkExpr' (mkExpr' k expr1) expr2
appCast :: forall a b c r. (Typeable a, Typeable b) = (c a - r) - c b -
r
appCast f x = maybe err f $ gcast x
where err = error $ Type error. Expected: ++ show (typeOf
(undefined::a))
++ , Inferred: ++ show (typeOf (undefined::b))
\end{code}
... We let Haskell do all the work!
=
Hmmm... the continuation can be anything.
So let's just make it an existential constructor.
\begin{code}
data ExprBox = forall a. Typeable a = ExprBox (Expr a)
appExprBox :: (forall a. Expr a - res) - ExprBox - res
Re: [Haskell-cafe] Manual Type-Checking to provide Read instances for GADTs. (was Re: [Haskell-cafe] Read instance for GATD)
I've obtained permission to repost Gershom's slides on how to deserialize
GADTs by typechecking them yourself, which are actually a literate haskell
source file, that he was rendering to slides. Consequently, I've just pasted
the content below as a literate email.
-Edward Kmett
-
Deserializing strongly typed values
(four easy pieces about typechecking)
Gershom Bazerman
-
prior art:
Oleg (of course)
http://okmij.org/ftp/tagless-final/course/course.html
...but also
Stephanie Weirich
http://www.comlab.ox.ac.uk/projects/gip/school/tc.hs
=
Ahem...
\begin{code}
{-# LANGUAGE DeriveDataTypeable,
ExistentialQuantification,
FlexibleContexts,
FlexibleInstances,
FunctionalDependencies,
GADTs,
RankNTypes,
ScopedTypeVariables
#-}
\end{code}
=
ahem.
\begin{code}
import Data.Typeable
import Data.Maybe
import Control.Monad.Error
import Control.Applicative
import qualified Data.Map as M
import Unsafe.Coerce
\end{code}
=
A simple ADT.
\begin{code}
data SimpleExpr = SOpBi String SimpleExpr SimpleExpr
| SOpUn String SimpleExpr
| SDbl Double
| SBool Bool deriving (Read, Show, Typeable)
\end{code}
Yawn.
=
An awesome GADT!
\begin{code}
data Expr a where
EDbl :: Double - Expr Double
EBool :: Bool - Expr Bool
EBoolOpBi :: BoolOpBi - Expr Bool - Expr Bool - Expr Bool
ENumOpBi :: NumOpBi - Expr Double - Expr Double - Expr Double
ENumOpUn :: NumOpUn - Expr Double - Expr Double
deriving Typeable
data NumOpBi = Add | Sub deriving (Eq, Show)
data NumOpUn = Log | Exp deriving (Eq, Show)
data BoolOpBi = And | Or deriving (Eq, Show)
\end{code}
The GADT is well typed. It cannot go wrong.
-
It also cannot derive show.
=
But we can write show...
\begin{code}
showIt :: Expr a - String
showIt (EDbl d) = show d
showIt (EBool b) = show b
showIt (EBoolOpBi op x y) = ( ++ show op
++ ++ showIt x
++ ++ showIt y ++ )
showIt (ENumOpBi op x y) = ( ++ show op
++ ++ showIt x
++ ++ showIt y ++ )
showIt (ENumOpUn op x) = show op ++ ( ++ showIt x ++ )
\end{code}
=
And eval is *much nicer*.
It cannot go wrong -- no runtime typechecks.
\begin{code}
evalIt :: Expr a - a
evalIt (EDbl x) = x
evalIt (EBool x) = x
evalIt (EBoolOpBi op expr1 expr2)
| op == And = evalIt expr1 evalIt expr2
| op == Or = evalIt expr2 || evalIt expr2
evalIt (ENumOpBi op expr1 expr2)
| op == Add = evalIt expr1 + evalIt expr2
| op == Sub = evalIt expr1 - evalIt expr2
\end{code}
=
But how do we write read!?
read EBool False = Expr Bool
read EDbl 12 = Expr Double
The type being read depends on the content of the string.
Even worse, we want to read not from a string that looks obvious
to Haskell (i.e. a standard showlike instance) but from
something that looks pretty to the user -- we want to *parse*.
So we parse into our simple ADT.
Then we turn our simple ADT into our nice GADT.
-
But how?
How do we go from untyped... to typed?
[And in general -- not just into an arbitrary GADT,
but an arbitrary inhabitant of a typeclass.]
[i.e. tagless final, etc]
=
Take 1:
Even if we do not know what type we are creating,
we eventually will do something with it.
So we paramaterize our typechecking function over
an arbitrary continuation.
\begin{code}
mkExpr :: (forall a. (Show a, Typeable a) = Expr a - r) - SimpleExpr - r
mkExpr k expr = case expr of
SDbl d - k $ EDbl d
SBool b - k $ EBool b
SOpUn op expr1 - case op of
log - k $ mkExpr' (ENumOpUn Log) expr1
exp - k $ mkExpr' (ENumOpUn Exp) expr1
_ - error bad unary op
SOpBi op expr1 expr2 - case op of
add - k $ mkExprBi (ENumOpBi Add) expr1 expr2
sub - k $ mkExprBi (ENumOpBi Sub) expr1 expr2
\end{code}
=
Where's the typechecking?
\begin{code}
mkExpr' k expr = mkExpr (appCast $ k) expr
mkExprBi k expr1 expr2 = mkExpr' (mkExpr' k expr1) expr2
appCast :: forall a b c r. (Typeable a, Typeable b) = (c a - r) - c b -
r
appCast f x = maybe err f $ gcast x
where err = error $ Type error. Expected: ++ show (typeOf
(undefined::a))
++ , Inferred: ++ show (typeOf (undefined::b))
\end{code}
... We let Haskell do all the work!
=
Hmmm... the continuation can be anything.
So let's just make it an existential constructor.
\begin{code}
data ExprBox = forall a. Typeable a = ExprBox (Expr a)
appExprBox :: (forall a. Expr a - res) - ExprBox - res
appExprBox f (ExprBox x) = f x
tcCast :: forall a b c. (Typeable a, Typeable b) = Expr a - Either String
(Expr b)
tcCast x = maybe err Right $ gcast x
where err = Left $ Type error. Expected: ++ show (typeOf
(undefined::a))
++ , Inferred: ++ show
[Haskell-cafe] Re: Non-termination of type-checking
And I'm pretty sure that there's no way to convince Agda that F = R, or something similar, because, despite the fact that Agda has injective type constructors like GHC (R x = R y = x = y), it doesn't let you make the inference R Unit = F Unit = R = F. Of course, in Agda, one could arguably say that it's true, because Agda has no type case, so there's (I'm pretty sure) no way to write an F such that R T = F T, but R U /= F U, for some U /= T. It's easy to construct an F that is different from R but agrees with R for the case of Unit: F = λ _ - R Unit So there's a good reason why Agda doesn't let F and R unify: it would really be completely wrong. Stefan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Non-termination of type-checking
We explain the technique of systematically deriving absurd terms and
apply it to type families.
Indeed I should have said that there is no _overt_ impredicative
polymorphism in the example posted earlier: it is precisely the
impredicative polymorphism that causes the paradox. As everybody
noticed, the example was an implementation of the Russell paradox
(whose elimination was the goal for the introduction of
predicativity).
Here is how the `absurd' example was derived. Our goal is to define a
recursive (rather than a mere inductive) data type, such as
data R = MkR (R - False)
If we have this data type, we can easily obtain the fixpoint
combinator, and hence logical inconsistency. But we want to avoid
overt recursive type. Therefore, we break the recursive knot, by
parameterizing R:
data R c = MkR (c - False)
The hope is that we can instantiate the type variable c with R and
recover the desired recursive type. The type variable c is thus
quantified over the set of types that include the type R being
defined. This impredicative polymorphism is essential for the trick.
However, instantiating the type variable c with R would be a kind
error: c has the kind * and R has the kind *-*. The obvious
work-around
data R c = MkR (c () - False)
fails: now c has the kind (*-*) but R has the kind
(*-*)-*. Again, R is not substitutable for c. If all we have are
ordinary data types, we are stuck -- for exactly the same reason that
self-application is not expressible in simply-typed lambda-calculus.
GADTs come to the rescue, giving us the needed `phase shift'. We can
define the datatype as (in pseudo-normal notation)
data R (c ()) = MkR (c () - False)
Now we can substitute R for c; alas, the result
data R (R ()) = MkR (R () - False)
is not the recursive type. The fix is trivial though:
data R (c ()) = MkR (c (c ()) - False)
Now that the method is clear, we derive the absurd term using type
functions (lest one thinks we are picking on GADTs). Type families too
let us introduce the `phase shift' (on the other side of the equation)
and thus bring about the destructive power of impredicativity.
Here is the complete code:
{-# LANGUAGE TypeFamilies, EmptyDataDecls #-}
data False-- No constructors
data I c = I (c ())
type family Interpret c :: *
type instance Interpret (I c) = c (I c)
data R c = MkR (Interpret c - False)
cond_false :: R (I R) - False
cond_false x@(MkR f) = f x
{- This diverges
absurd :: False
absurd = cond_false (MkR cond_false)
-}
-- Thanks to Martin Sulzmann
absurd2 :: False
absurd2 = let x = MkR cond_false in cond_false x
It seems likely `absurd' diverges in GHCi is because of the GHC
inliner. The paper about secrets of the inliner points out that the
aggressiveness of the inliner can cause divergence in the compiler
when processing code with negative recursive types. Probably GHCi
internally derives the recursive equation when processing the instance
R (I R) of the data type R.
Dan Doel wrote:
Anyhow, I don't particularly find this 'scary', as Haskell/GHC isn't
attempting to be an environment for theorem proving, and being able to encode
(\x - x x) (\x - x x) through lack of logical consistency isn't giving up
anything that hasn't already been given up multiple times (through general
recursion, error and negative types at least).
I agree. Still, it would be nice not to give up logical consistency
one more time. More interesting is to look at the languages that are
designed for theorem proving. How many of them have impredicative
polymorphism? Are we certain other features of the language, such as
type functions (specifically, case analysis) don't introduce the phase
shift that unleashes the impredicativity?
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Non-termination of type-checking
Thanks for the clear explanation, oleg.
-- ryan
On Sat, Jan 30, 2010 at 12:44 AM, o...@okmij.org wrote:
We explain the technique of systematically deriving absurd terms and
apply it to type families.
Indeed I should have said that there is no _overt_ impredicative
polymorphism in the example posted earlier: it is precisely the
impredicative polymorphism that causes the paradox. As everybody
noticed, the example was an implementation of the Russell paradox
(whose elimination was the goal for the introduction of
predicativity).
Here is how the `absurd' example was derived. Our goal is to define a
recursive (rather than a mere inductive) data type, such as
data R = MkR (R - False)
If we have this data type, we can easily obtain the fixpoint
combinator, and hence logical inconsistency. But we want to avoid
overt recursive type. Therefore, we break the recursive knot, by
parameterizing R:
data R c = MkR (c - False)
The hope is that we can instantiate the type variable c with R and
recover the desired recursive type. The type variable c is thus
quantified over the set of types that include the type R being
defined. This impredicative polymorphism is essential for the trick.
However, instantiating the type variable c with R would be a kind
error: c has the kind * and R has the kind *-*. The obvious
work-around
data R c = MkR (c () - False)
fails: now c has the kind (*-*) but R has the kind
(*-*)-*. Again, R is not substitutable for c. If all we have are
ordinary data types, we are stuck -- for exactly the same reason that
self-application is not expressible in simply-typed lambda-calculus.
GADTs come to the rescue, giving us the needed `phase shift'. We can
define the datatype as (in pseudo-normal notation)
data R (c ()) = MkR (c () - False)
Now we can substitute R for c; alas, the result
data R (R ()) = MkR (R () - False)
is not the recursive type. The fix is trivial though:
data R (c ()) = MkR (c (c ()) - False)
Now that the method is clear, we derive the absurd term using type
functions (lest one thinks we are picking on GADTs). Type families too
let us introduce the `phase shift' (on the other side of the equation)
and thus bring about the destructive power of impredicativity.
Here is the complete code:
{-# LANGUAGE TypeFamilies, EmptyDataDecls #-}
data False -- No constructors
data I c = I (c ())
type family Interpret c :: *
type instance Interpret (I c) = c (I c)
data R c = MkR (Interpret c - False)
cond_false :: R (I R) - False
cond_false x@(MkR f) = f x
{- This diverges
absurd :: False
absurd = cond_false (MkR cond_false)
-}
-- Thanks to Martin Sulzmann
absurd2 :: False
absurd2 = let x = MkR cond_false in cond_false x
It seems likely `absurd' diverges in GHCi is because of the GHC
inliner. The paper about secrets of the inliner points out that the
aggressiveness of the inliner can cause divergence in the compiler
when processing code with negative recursive types. Probably GHCi
internally derives the recursive equation when processing the instance
R (I R) of the data type R.
Dan Doel wrote:
Anyhow, I don't particularly find this 'scary', as Haskell/GHC isn't
attempting to be an environment for theorem proving, and being able to encode
(\x - x x) (\x - x x) through lack of logical consistency isn't giving up
anything that hasn't already been given up multiple times (through general
recursion, error and negative types at least).
I agree. Still, it would be nice not to give up logical consistency
one more time. More interesting is to look at the languages that are
designed for theorem proving. How many of them have impredicative
polymorphism? Are we certain other features of the language, such as
type functions (specifically, case analysis) don't introduce the phase
shift that unleashes the impredicativity?
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Non-termination of type-checking
On Saturday 30 January 2010 3:44:35 am o...@okmij.org wrote:
It seems likely `absurd' diverges in GHCi is because of the GHC
inliner. The paper about secrets of the inliner points out that the
aggressiveness of the inliner can cause divergence in the compiler
when processing code with negative recursive types. Probably GHCi
internally derives the recursive equation when processing the instance
R (I R) of the data type R.
I've even observed your prior code hang when loading into GHCi, though. Does
inlining get done even for byte code, with no -O?
I agree. Still, it would be nice not to give up logical consistency
one more time. More interesting is to look at the languages that are
designed for theorem proving. How many of them have impredicative
polymorphism? Are we certain other features of the language, such as
type functions (specifically, case analysis) don't introduce the phase
shift that unleashes the impredicativity?
Coq has an impredicative universe of propositions, and Agda has a --type-in-
type option (which is definitely inconsistent), allowing both to encode your
systematically derived type. However, neither allow one to actually well type
(\x - x x) (\x - x x) by this method. In Agda:
{-# OPTIONS --type-in-type --injective-type-constructors #-}
module Stuff where
data False : Set where
data Unit : Set where
unit : Unit
data R : Set → Set where
r : (F : Set → Set) → (F (F Unit) → False) → R (F Unit)
w : R (R Unit) → False
w x with R Unit | x
... | ._ | r F f = {! !}
The with stuff can be ignored; that's required get Agda to allow matching on
x for some reason. Anyhow, we need to fill in the hole delimited by the {! !}
with something of type False, but what we have are:
x : R (R Unit)
f : F (F Unit) - False
And I'm pretty sure that there's no way to convince Agda that F = R, or
something similar, because, despite the fact that Agda has injective type
constructors like GHC (R x = R y = x = y), it doesn't let you make the
inference R Unit = F Unit = R = F. Of course, in Agda, one could arguably say
that it's true, because Agda has no type case, so there's (I'm pretty sure) no
way to write an F such that R T = F T, but R U /= F U, for some U /= T.
But, in GHC, where you *do* have type case, and *can* write functions like the
above, GHC lets you infer that R = F anyway, and throws type errors when
trying to build elements of R (T ()) for T () = R () but T /= R.
I'm relatively sure Coq is in the same boat as Agda. I've successfully defined
R above as a Prop, using impredicativity, but I'm pretty sure you'll run into
the same difficulty trying to write w there (but I don't know Coq well enough
to give a demonstration).
Coq doesn't give injectivity of type constructors by fiat, which is good,
because it can be used with impredicativity to write other paradoxes (just not
the one above). Agda has the injectivity,* but not the impredicativity. Also,
this all originally came (I believe) from the Agda mailing list, where someone
demonstrated that injectivity of type constructors is inconsistent with a
certain version of the law of the excluded middle.** However, the paradox
above seems to be unique to GHC (among the three), which is rather odd.
-- Dan
* Injectivity of type constructors is now optional in Agda, turned on by the
flag you can see above.
** Injectivity of type constructors allows you to write a proof of:
¬ (∀ (P : Set1) → P ∨ ¬ P)
there was some concern raised, because in intuitionistic logic, one can prove:
∀ (P : Set1) → ¬ ¬ (P ∨ ¬ P)
But, the above two propositions aren't contradictory, because one can't move
the quantifier past the negations as one could in classical logic. Coq in fact
allows one to prove something similar to the first proposition with --
impredicative-set, which led to that being off by default (so that one could
take excluded middle as an axiom and do classical reasoning without
(hopefully) introducing inconsistency).
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Non-termination of type-checking
On Thu, 28 Jan 2010 18:32:02 -0800, Ryan Ingram ryani.s...@gmail.com wrote: But your example uses a recursive type; the interesting bit about this example is that there is no recursive types or function, and yet we can encode this loop. The point is that you get the Fix type by (infintely) unfolding the type definitions. -- Nicolas Pouillard http://nicolaspouillard.fr ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Non-termination of type-checking
On Friday 29 January 2010 2:56:31 am o...@okmij.org wrote:
Here is a bit more simplified version of the example. The example has
no value level recursion and no overt recursive types, and no impredicative
polymorphism. The key is the observation, made earlier, that two types
c (c ()) and R (c ())
unify when c = R. Although the GADTs R c below is not recursive, when
we instantiate c = R, it becomes recursive, with the negative
occurrence. The trouble is imminent.
We reach the conclusion that an instance of a non-recursive GADT
can be a recursive type. GADT may harbor recursion, so to speak.
The code below, when loaded into GHCi 6.10.4, diverges on
type-checking. It type-checks when we comment-out absurd.
{-# LANGUAGE GADTs, EmptyDataDecls #-}
data False-- No constructors
data R c where-- Not recursive
R :: (c (c ()) - False) - R (c ())
-- instantiate c to R, so (c (c ())) and R (c ()) coincide
-- and we obtain a recursive type
--mu R. (R (R ()) - False) - R (R ())
cond_false :: R (R ()) - False
cond_false x@(R f) = f x
absurd :: False
absurd = cond_false (R cond_false)
This example is pretty weird in my view. For instance, consider:
data S x
type family T x :: *
type family T () = R ()
type family T (R ()) = S ()
s'elim :: S x - False
s'elim x = undefined -- case x of {}
what :: T (T ()) - False
what = s'elim
Now, we have T () ~ R (), and T (T ()) ~ S (R ()), so R (T ()) ~ R (R ()), no?
And T :: * - *, so it should be an acceptable argument to R. So, one would
expect that I could write:
r :: R (R ()) -- R (T ())
r = R what
However, neither of those signatures for r goes through. With the second, I
get a complaint that:
Couldn't match expected type `S ()' against inferred type `()'
Expected type: S (S ())
Inferred type: T (T ())
though I'm not quite sure how it gets that error. With the R (R ()) choice, I
get:
Couldn't match expected type `R (R ())'
against inferred type `T (T ())'
NB: `T' is a type function, and may not be injective
but the injectivity GHC seems to be relying on isn't F x ~ F y = x ~ y, but:
f T ~ g T = f ~ g
or injectivity of ($ ()) in this case, so to speak. But this seems like a
significantly weirder thing to take for granted than injectivity of type
constructors. I suppose it's sufficient to limit c (in the constructor R's
definition) to accept only data type constructors, but that's significantly
more limiting than I'd expect to be the case (although, it does appear to be
what GHC does).
Anyhow, I don't particularly find this 'scary', as Haskell/GHC isn't
attempting to be an environment for theorem proving, and being able to encode
(\x - x x) (\x - x x) through lack of logical consistency isn't giving up
anything that hasn't already been given up multiple times (through general
recursion, error and negative types at least). Non-termination of type
checking is undesirable, of course.
-- Dan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Non-termination of type-checking
On Fri, Jan 29, 2010 at 8:56 AM, o...@okmij.org wrote:
Here is a bit more simplified version of the example. The example has
no value level recursion and no overt recursive types, and no impredicative
polymorphism. The key is the observation, made earlier, that two types
c (c ()) and R (c ())
unify when c = R. Although the GADTs R c below is not recursive, when
we instantiate c = R, it becomes recursive, with the negative
occurrence. The trouble is imminent.
We reach the conclusion that an instance of a non-recursive GADT
can be a recursive type. GADT may harbor recursion, so to speak.
The code below, when loaded into GHCi 6.10.4, diverges on
type-checking. It type-checks when we comment-out absurd.
{-# LANGUAGE GADTs, EmptyDataDecls #-}
data False -- No constructors
data R c where -- Not recursive
R :: (c (c ()) - False) - R (c ())
-- instantiate c to R, so (c (c ())) and R (c ()) coincide
-- and we obtain a recursive type
--mu R. (R (R ()) - False) - R (R ())
cond_false :: R (R ()) - False
cond_false x@(R f) = f x
absurd :: False
absurd = cond_false (R cond_false)
GHC (the compiler terminates)
The following variants terminate, either with GHCi or GHC,
absurd1 :: False
absurd1 = let x = (R cond_false)
in cond_false x
absurd2 = R cond_false
absurd3 x = cond_false x
absurd4 :: False
absurd4 = absurd3 absurd2
This suggests there's a bug in the type checker.
If i scribble down the type equation, I can't see
why the type checker should loop here.
-Martin
___
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] Re: Non-termination of type-checking
Le 29 janv. 10 à 02:56, o...@okmij.org a écrit :
Here is a bit more simplified version of the example. The example has
no value level recursion and no overt recursive types, and no
impredicative
polymorphism. The key is the observation, made earlier, that two types
c (c ()) and R (c ())
unify when c = R. Although the GADTs R c below is not recursive, when
we instantiate c = R, it becomes recursive, with the negative
occurrence. The trouble is imminent.
We reach the conclusion that an instance of a non-recursive GADT
can be a recursive type. GADT may harbor recursion, so to speak.
The code below, when loaded into GHCi 6.10.4, diverges on
type-checking. It type-checks when we comment-out absurd.
{-# LANGUAGE GADTs, EmptyDataDecls #-}
data False -- No constructors
data R c where -- Not recursive
R :: (c (c ()) - False) - R (c ())
Thanks Oleg,
that's a bit simpler indeed. However, I'm skeptical on
the scoping of c here. Correct me if I'm wrong but in R's
constructor [c] is applied to () so it has to be a type
constructor variable of kind :: * - s. But [c] is also
applied to [c ()] so we must have s = * and c :: * - *.
Now given the application [R (c ())] we must have
[R :: * - *]. Then in [data R c] we must have [c :: *],
hence a contradiction?
My intuition would be that the declaration is informally
equivalent to the impredicative:
data R (c :: *) where
R :: forall c' :: * - *, (c' (c' ()) - False) - R (c' ()).
-- Matthieu___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Non-termination of type-checking
On Friday 29 January 2010 5:26:28 pm Matthieu Sozeau wrote: data R (c :: *) where R :: forall c' :: * - *, (c' (c' ()) - False) - R (c' ()). This is what the data declaration is. The c on the first line and the c on the second line are unrelated. It's sort of an oddity of GADT declarations; variables used between the 'data' and 'where' are just placeholders. With KindSignatures enabled, one could also write: data R :: * - * where R :: (c (c ()) - False) - R (c ()) or explicitly quantify c in the constructor's type. That confused me at first, as well. -- Dan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Non-termination of type-checking
Am Freitag 29 Januar 2010 23:26:28 schrieb Matthieu Sozeau:
Le 29 janv. 10 à 02:56, o...@okmij.org a écrit :
Here is a bit more simplified version of the example. The example has
no value level recursion and no overt recursive types, and no
impredicative
polymorphism. The key is the observation, made earlier, that two types
c (c ()) and R (c ())
unify when c = R. Although the GADTs R c below is not recursive, when
we instantiate c = R, it becomes recursive, with the negative
occurrence. The trouble is imminent.
We reach the conclusion that an instance of a non-recursive GADT
can be a recursive type. GADT may harbor recursion, so to speak.
The code below, when loaded into GHCi 6.10.4, diverges on
type-checking. It type-checks when we comment-out absurd.
{-# LANGUAGE GADTs, EmptyDataDecls #-}
data False -- No constructors
data R c where -- Not recursive
R :: (c (c ()) - False) - R (c ())
Thanks Oleg,
that's a bit simpler indeed. However, I'm skeptical on
the scoping of c here.
The c in data R c has nothing to do with the c in
R :: (c (c ()) - False) - R (c ())
It would probably have been less confusing to declare it
data R :: * - * where
R :: (c (c ()) - False) - R (c ())
Correct me if I'm wrong but in R's
constructor [c] is applied to () so it has to be a type
constructor variable of kind :: * - s. But [c] is also
applied to [c ()] so we must have s = * and c :: * - *.
Now given the application [R (c ())] we must have
[R :: * - *]. Then in [data R c] we must have [c :: *],
hence a contradiction?
My intuition would be that the declaration is informally
equivalent to the impredicative:
data R (c :: *) where
R :: forall c' :: * - *, (c' (c' ()) - False) - R (c' ()).
-- Matthieu
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Non-termination of type-checking
But your example uses a recursive type; the interesting bit about this
example is that there is no recursive types or function, and yet we
can encode this loop.
-- ryan
On Wed, Jan 27, 2010 at 4:49 PM, Matthew Brecknell
matt...@brecknell.net wrote:
Ryan Ingram wrote:
The compiler doesn't loop for me with GHC6.10.4; I think GADTs still
had some bugs in GHC6.8.
That said, this is pretty scary. Here's a simplified version that
shows this paradox with just a single GADT and no other extensions.
No use of fix or recursion anywhere!
{-# LANGUAGE GADTs #-}
module Contr where
newtype I f = I (f ())
data R o a where R :: (a (I a) - o) - R o (I a)
run :: R o (I (R o)) - R o (I (R o)) - o
run x (R f) = f x
rir :: (R o) (I (R o))
rir = R (\x - run x x)
absurd :: a
absurd = run rir rir
I think that's essentially the same as this:
data Fix a = Fix { unFix :: Fix a - a }
run :: Fix a - Fix a - a
run x f = unFix f x
rir :: Fix a
rir = Fix (\x - run x x)
absurd :: a
absurd = run rir rir
Non-positive recursive occurrences in type definitions provide various
ways to encode the Y-combinator in a typed lambda calculus, without the
need for any recursive let primitive. Haskell allows such non-positive
occurrences, but for strong normalisation, languages like Coq must
disallow them.
If you change data to newtype in the above, the GHC 6.10.4 compiler
(but not GHCi) will loop. I think this is just a case of the infelicity
documented here:
http://www.haskell.org/ghc/docs/latest/html/users_guide/bugs.html
Regards,
Matthew
___
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] Re: Non-termination of type-checking
Here is a bit more simplified version of the example. The example has
no value level recursion and no overt recursive types, and no impredicative
polymorphism. The key is the observation, made earlier, that two types
c (c ()) and R (c ())
unify when c = R. Although the GADTs R c below is not recursive, when
we instantiate c = R, it becomes recursive, with the negative
occurrence. The trouble is imminent.
We reach the conclusion that an instance of a non-recursive GADT
can be a recursive type. GADT may harbor recursion, so to speak.
The code below, when loaded into GHCi 6.10.4, diverges on
type-checking. It type-checks when we comment-out absurd.
{-# LANGUAGE GADTs, EmptyDataDecls #-}
data False -- No constructors
data R c where -- Not recursive
R :: (c (c ()) - False) - R (c ())
-- instantiate c to R, so (c (c ())) and R (c ()) coincide
-- and we obtain a recursive type
--mu R. (R (R ()) - False) - R (R ())
cond_false :: R (R ()) - False
cond_false x@(R f) = f x
absurd :: False
absurd = cond_false (R cond_false)
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Non-termination of type-checking
Dear Haskellers,
while trying to encode a paradox recently found in Coq if one has
impredicativity and adds injectivity of type constructors [1] I
stumbled on an apparent loop in the type checker when using GADTs,
Rank2Types and EmptyDataDecls.
{-# OPTIONS -XGADTs -XRank2Types -XEmptyDataDecls #-}
module Impred where
The identity type
data ID a = ID a
I is from (* - *) to *, we use a partial application of [ID] here.
data I f where
I1 :: I ID
The usual reification of type equality into a term.
data Equ a b where
Eqrefl :: Equ a a
The empty type
data False
This uses impredicativity: Rdef embeds a (* - *) - *
object into R x :: *.
data R x where
Rdef :: (forall a. Equ x (I a) - a x - False) - R x
r_eqv1 :: forall p. R (I p) - p (I p) - False
r_eqv1 (Rdef f) pip = f Eqrefl pip
r_eqv2 :: forall p. (p (I p) - False) - R (I p)
r_eqv2 f = Rdef (\ eq ax -
case eq of -- Uses injectivity of type
constructors
Eqrefl - f ax)
r_eqv_not_R_1 :: R (I R) - R (I R) - False
r_eqv_not_R_1 = r_eqv1
r_eqv_not_R_2 :: (R (I R) - False) - R (I R)
r_eqv_not_R_2 = r_eqv2
rir :: R (I R)
rir = r_eqv_not_R_2 (\ rir - r_eqv_not_R_1 rir rir)
Type checking seems to loop here with ghc-6.8.3, which is a
bit strange given the simplicity of the typing problem.
Maybe it triggers a constraint with something above?
-- Loops
-- absurd :: False
-- absurd = r_eqv_not_R_1 rir rir
[1]
http://thread.gmane.org/gmane.science.mathematics.logic.coq.club/4322/focus=1405
-- Matthieu
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Non-termination of type-checking
The compiler doesn't loop for me with GHC6.10.4; I think GADTs still
had some bugs in GHC6.8.
That said, this is pretty scary. Here's a simplified version that
shows this paradox with just a single GADT and no other extensions.
No use of fix or recursion anywhere!
{-# LANGUAGE GADTs #-}
module Contr where
newtype I f = I (f ())
data R o a where R :: (a (I a) - o) - R o (I a)
run :: R o (I (R o)) - R o (I (R o)) - o
run x (R f) = f x
rir :: (R o) (I (R o))
rir = R (\x - run x x)
absurd :: a
absurd = run rir rir
-- ryan
On Wed, Jan 27, 2010 at 8:27 AM, Matthieu Sozeau mat...@mattam.org wrote:
Dear Haskellers,
while trying to encode a paradox recently found in Coq if one has
impredicativity and adds injectivity of type constructors [1] I
stumbled on an apparent loop in the type checker when using GADTs,
Rank2Types and EmptyDataDecls.
{-# OPTIONS -XGADTs -XRank2Types -XEmptyDataDecls #-}
module Impred where
The identity type
data ID a = ID a
I is from (* - *) to *, we use a partial application of [ID] here.
data I f where
I1 :: I ID
The usual reification of type equality into a term.
data Equ a b where
Eqrefl :: Equ a a
The empty type
data False
This uses impredicativity: Rdef embeds a (* - *) - *
object into R x :: *.
data R x where
Rdef :: (forall a. Equ x (I a) - a x - False) - R x
r_eqv1 :: forall p. R (I p) - p (I p) - False
r_eqv1 (Rdef f) pip = f Eqrefl pip
r_eqv2 :: forall p. (p (I p) - False) - R (I p)
r_eqv2 f = Rdef (\ eq ax -
case eq of -- Uses injectivity of type constructors
Eqrefl - f ax)
r_eqv_not_R_1 :: R (I R) - R (I R) - False
r_eqv_not_R_1 = r_eqv1
r_eqv_not_R_2 :: (R (I R) - False) - R (I R)
r_eqv_not_R_2 = r_eqv2
rir :: R (I R)
rir = r_eqv_not_R_2 (\ rir - r_eqv_not_R_1 rir rir)
Type checking seems to loop here with ghc-6.8.3, which is a
bit strange given the simplicity of the typing problem.
Maybe it triggers a constraint with something above?
-- Loops
-- absurd :: False
-- absurd = r_eqv_not_R_1 rir rir
[1]
http://thread.gmane.org/gmane.science.mathematics.logic.coq.club/4322/focus=1405
-- Matthieu
___
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] Non-termination of type-checking
Ryan Ingram wrote:
The compiler doesn't loop for me with GHC6.10.4; I think GADTs still
had some bugs in GHC6.8.
That said, this is pretty scary. Here's a simplified version that
shows this paradox with just a single GADT and no other extensions.
No use of fix or recursion anywhere!
{-# LANGUAGE GADTs #-}
module Contr where
newtype I f = I (f ())
data R o a where R :: (a (I a) - o) - R o (I a)
run :: R o (I (R o)) - R o (I (R o)) - o
run x (R f) = f x
rir :: (R o) (I (R o))
rir = R (\x - run x x)
absurd :: a
absurd = run rir rir
I think that's essentially the same as this:
data Fix a = Fix { unFix :: Fix a - a }
run :: Fix a - Fix a - a
run x f = unFix f x
rir :: Fix a
rir = Fix (\x - run x x)
absurd :: a
absurd = run rir rir
Non-positive recursive occurrences in type definitions provide various
ways to encode the Y-combinator in a typed lambda calculus, without the
need for any recursive let primitive. Haskell allows such non-positive
occurrences, but for strong normalisation, languages like Coq must
disallow them.
If you change data to newtype in the above, the GHC 6.10.4 compiler
(but not GHCi) will loop. I think this is just a case of the infelicity
documented here:
http://www.haskell.org/ghc/docs/latest/html/users_guide/bugs.html
Regards,
Matthew
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Naive booleans and numbers - type-checking fails
As other people have said, you need higher rank types for this.
Lets start with just pairs to get you headed in the right direction:
{-# LANGUAGE RankNTypes #-}
(As an aside, almost all of my real programs require at least rank-2
types, so I usually turn on RankNTypes on principle)
mpair :: a - b - (a - b - c) - c
mpair f s k = k f s
mfst p = p (\x y - x)
msnd p = p (\x y - y)
Here is where it gets tricky. GHC infers these types:
mfst :: ((a - b - a) - c) - c
msnd :: ((a - b - b) - c) - c
But these aren't the right types; if you try to use both mfst and msnd
on the same pair, you will unify a and b which is almost certainly
wrong; it says the first and second element of the pair are the same
type.
Now, lets look at the type signature for the partially-applied mpair;
given x :: A, and y :: B, we have
mpair x y :: (A - B - c) - c
Notice this: a pair is a polymorphic function! Lets make functions
that take pairs specify that explicitly:
mfst :: (forall c. (a - b - c) - c) - a
msnd :: (forall c. (a - b - c) - c) - b
Here we tell the typechecker that mfst and msnd are required to be
passed polymorphic functions; this makes us free to determine the
result type when we call p, and the same pair can be passed to both
of these functions successfully. The placement of the parentheses
around the forall is very important, because that's how we specify
where the polymorphism is required.
Similar tricks generally need to be used when defining church
numerals, if you are headed in that direction. These sort of objects
which work in untyped lambda calculus are just not expressible in the
simply typed lambda calculus, even with rank-1 polymorphism. Once you
move to full System F, a lot more becomes possible.
-- ryan
2010/1/24 Dušan Kolář ko...@fit.vutbr.cz:
Dear cafe,
I'm trying to prepare a naive definition of booleans, numbers and some
helper functions such a way, so that definition in lambda-calculus can be
used in a straightforward way in Haskell. I was caught in trouble quite soon
during change of lambda-expressions to Haskell - defining prefn as a helper
for prev. When using Haskell-ish if-then-else then there is no problem (the
code commented out), while using defined if-then-else (mif), the
type-checking fails, but just for this case! Other simple tests are OK for
the mif. Do I need some extra option for type-checker, or is it a principal
failure (infinite type is reported) - I'm running ghci 6.10.4.
mtrue x y = x
mfalse x y = y
m0 f n = n
m1 f n = f n
m2 f n = f (f n)
msucc x g m = x g (g m)
iszero m = m (\_ - mfalse) mtrue
mif c t f = c t f
mpair f s = \e - e f s
mfst p = p mtrue
msnd p = p mfalse
-- mprefn f p = if mex True False then mth else mel
mprefn f p = mif mex mth mel
where
mex = mfst p
mth = mpair mfalse (msnd p)
mel = mpair mfalse (f (msnd p))
Please, change of definitions is not a solution, I'm trying to follow
available resources, so using something else is not an option. :-(
Thanks for any help
Dusan
___
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] Naive booleans and numbers - type-checking fails
Dear cafe, I'm trying to prepare a naive definition of booleans, numbers and some helper functions such a way, so that definition in lambda-calculus can be used in a straightforward way in Haskell. I was caught in trouble quite soon during change of lambda-expressions to Haskell - defining prefn as a helper for prev. When using Haskell-ish if-then-else then there is no problem (the code commented out), while using defined if-then-else (mif), the type-checking fails, but just for this case! Other simple tests are OK for the mif. Do I need some extra option for type-checker, or is it a principal failure (infinite type is reported) - I'm running ghci 6.10.4. mtrue x y = x mfalse x y = y m0 f n = n m1 f n = f n m2 f n = f (f n) msucc x g m = x g (g m) iszero m = m (\_ - mfalse) mtrue mif c t f = c t f mpair f s = \e - e f s mfst p = p mtrue msnd p = p mfalse -- mprefn f p = if mex True False then mth else mel mprefn f p = mif mex mth mel where mex = mfst p mth = mpair mfalse (msnd p) mel = mpair mfalse (f (msnd p)) Please, change of definitions is not a solution, I'm trying to follow available resources, so using something else is not an option. :-( Thanks for any help Dusan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Naive booleans and numbers - type-checking fails
Doesn't the simply typed lambda calculus introduce if-then-else as a primitive precisely so that it can be typed? Its not an illuminating answer to your question and I'd welcome clarification for my own understanding, but I don't think you can solve the problem without appealing to Haskell's built-in if-then-else. Best wishes Stephen ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Naive booleans and numbers - type-checking fails
On Sun, Jan 24, 2010 at 3:12 PM, Stephen Tetley stephen.tet...@gmail.com wrote: Doesn't the simply typed lambda calculus introduce if-then-else as a primitive precisely so that it can be typed? Its not an illuminating answer to your question and I'd welcome clarification for my own understanding, but I don't think you can solve the problem without appealing to Haskell's built-in if-then-else. Yes, encoding data types as pure typed lambda terms requires rank-2 types. I'd recommend that Dušan Kolář start giving types to all these functions. However, it will, eventually, be necessary to go beyond Haskell 98 to give the appropriate types. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Exponential complexity of type checking (Was: Type-level naturals multiplication)
You can help ghci out a bit with type synonyms: type T a = (a, a) type T2 a = T (T a) type T4 a = T2 (T2 a) type T8 a = T4 (T4 a) type T16 a = T8 (T8 a) f0 :: a - T a f1 :: a - T2 a f2 :: a - T4 a f3 :: a - T8 a f4 :: a - T16 a f0 x = (x,x) f1 = f0 . f0 f2 = f1 . f1 f3 = f2 . f2 f4 = f3 . f3 f5 = f4 . f4 With newtypes I can probably abstract even more. (newtype X a b = X (a (a b)) Inferring the type of f5 also stops my machine in its tracks. But I *was* able to infer the type of (f4 . f4). :t (f4 . f4) (f4 . f4) :: a - T16 (T16 a) :t f5 -- buy new computer Even when you only specify a type for f0 in terms of T you'll get more readable types: :t f3 f3 :: a - T (T (T (T (T (T (T (T a))) But the amount of computation required seems the same. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Exponential complexity of type checking (Was: Type-level naturals multiplication)
On Wednesday 14 October 2009 5:25:10 am Roel van Dijk wrote:
With newtypes I can probably abstract even more. (newtype X a b = X (a (a
b))
In fact, with GHC extensions, you don't need newtypes:
{-# LANGUAGE LiberalTypeSynonyms #-}
type T a = (a,a)
type X f a = f (f a)
f0 :: a - T a
f0 x = (x,x)
f1 :: a - X T a
f1 = f0 . f0
f2 :: a - X (X T) a
f2 = f1 . f1
f3 :: a - X (X (X T)) a
f3 = f2 . f2
f4 :: a - X (X (X (X T))) a
f4 = f3 . f3
Inferring the type of f5 also stops my machine in its tracks. But I
*was* able to infer the type of (f4 . f4).
:t (f4 . f4)
(f4 . f4) :: a - T16 (T16 a)
:t f5
Yeah. Asking for the type of 'f4 . f4' doesn't seem to expand the synonyms,
while checking f5 does for some reason. I'm perplexed that having f5 defined
in the file doesn't trigger the explosion unless you declare a type (even in
terms of X and T) or ask for its type at the prompt.
-- Dan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Exponential complexity of type checking (Was: Type-level naturals multiplication)
On Wed, Oct 14, 2009 at 11:53 AM, Dan Doel dan.d...@gmail.com wrote:
In fact, with GHC extensions, you don't need newtypes:
{-# LANGUAGE LiberalTypeSynonyms #-}
Ah, I completely forgot about that language extension. Thanks!
Yeah. Asking for the type of 'f4 . f4' doesn't seem to expand the synonyms,
while checking f5 does for some reason. I'm perplexed that having f5 defined
in the file doesn't trigger the explosion unless you declare a type (even in
terms of X and T) or ask for its type at the prompt.
If you declare a type for f5 then ghci must check if that type is
correct, which triggers the explosion. If you don't declare a type
then it won't infer the type until necessary. Basically, ghci is lazy
:-)
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Exponential complexity of type checking (Was: Type-level naturals multiplication)
On Wednesday 14 October 2009 6:15:11 am Roel van Dijk wrote: If you declare a type for f5 then ghci must check if that type is correct, which triggers the explosion. If you don't declare a type then it won't infer the type until necessary. Basically, ghci is lazy Well, that may be the explanation, but it's a bit more convoluted than I'd have initially thought. For instance, if I write: e = head () it fails immediately with a type error, so clearly it must be doing some level of checking immediately. However, it only needs to check 'head' and '()' to notice that they're incompatible, so I suppose it may not need to compute the type of e (were it well-typed). But then, adding: f6 = f5 . f5 produces no more delay than before. Nor does: g = snd . f5 So ghci is able to verify that f5 can be instantiated to the forms a - b and b - c in the first case, and that it is of the form a - (b,c) in the second case, without blowing up. However, either of: e = f5 () e' () = f5 () does blow up, so it must be verifying more than the fact that f5 is of the form a - b, where a can be instantiated to (), which is odd if it's smart enough to only compute the portion of the type necessary to verify that applications can be well typed. -- Dan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Exponential complexity of type checking (Was: Type-level naturals multiplication)
On Tue, Oct 13, 2009 at 3:37 AM, Simon Peyton-Jones simo...@microsoft.com wrote: | Is there any way to define type-level multiplication without requiring | undecidable instances? | | No, not at the moment. The reasons are explained in the paper Type | Checking with Open Type Functions (ICFP'08): | | http://www.cse.unsw.edu.au/~chak/papers/tc-tfs.pdf | | We want to eventually add closed *type families* to the system (ie, | families where you can't add new instances in other modules). For | such closed families, we should be able to admit more complex | instances without requiring undecidable instances. It's also worth noting that while undecidable instances sound scary, but all it means is that the type checker can't prove that type inference will terminate. We accept this lack-of-guarantee for the programs we *run*, and type inference can (worst case) take exponential time which is not so different from failing to terminate; so risking non-termination in type inference is arguably not so bad. Simon I have written code that makes heavy use of multi-parameter type classes in the ``finally tagless'' tradition, which takes several seconds and many megabytes of memory for GHCI to infer its type. However, that example is rather complicated, and I am not sure its type inference complexity is exponential---it is at least very bad. Are there any simple, well-known examples where Haskell type inference has exponential complexity? Or Hindley-Milner type inference, for that matter? (Haskell 98 is not quite Hindley-Milner?) Sincerely, Brad Larsen ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Exponential complexity of type checking (Was: Type-level naturals multiplication)
Yes, there are simple H-M examples that are exponential. x0 = undefined x1 = (x1,x1) x2 = (x2,x2) x3 = (x3,x3) ... xn will have a type with 2^n type variables so it has size 2^n. -- Lennart On Tue, Oct 13, 2009 at 6:04 PM, Brad Larsen brad.lar...@gmail.com wrote: On Tue, Oct 13, 2009 at 3:37 AM, Simon Peyton-Jones simo...@microsoft.com wrote: | Is there any way to define type-level multiplication without requiring | undecidable instances? | | No, not at the moment. The reasons are explained in the paper Type | Checking with Open Type Functions (ICFP'08): | | http://www.cse.unsw.edu.au/~chak/papers/tc-tfs.pdf | | We want to eventually add closed *type families* to the system (ie, | families where you can't add new instances in other modules). For | such closed families, we should be able to admit more complex | instances without requiring undecidable instances. It's also worth noting that while undecidable instances sound scary, but all it means is that the type checker can't prove that type inference will terminate. We accept this lack-of-guarantee for the programs we *run*, and type inference can (worst case) take exponential time which is not so different from failing to terminate; so risking non-termination in type inference is arguably not so bad. Simon I have written code that makes heavy use of multi-parameter type classes in the ``finally tagless'' tradition, which takes several seconds and many megabytes of memory for GHCI to infer its type. However, that example is rather complicated, and I am not sure its type inference complexity is exponential---it is at least very bad. Are there any simple, well-known examples where Haskell type inference has exponential complexity? Or Hindley-Milner type inference, for that matter? (Haskell 98 is not quite Hindley-Milner?) Sincerely, Brad Larsen ___ 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] Exponential complexity of type checking (Was: Type-level naturals multiplication)
2009/10/13 Lennart Augustsson lenn...@augustsson.net: Yes, there are simple H-M examples that are exponential. x0 = undefined x1 = (x1,x1) x2 = (x2,x2) x3 = (x3,x3) ... xn will have a type with 2^n type variables so it has size 2^n. Reformulated: let dup x = (x,x) :t dup . dup . dup . dup ... type will be 2^(number of dup's). I experimented and found that GHC can stand pretty long line of dup's. More than 20, at least. One part of our program took too much time to typecheck some time ago. 3 and half minutes for ~900 lines module. Most of operations was inside heavily parametrized monad (5 parameters, each is a Peano number). Then my colleague moved parameters into associated types of relevant type class and now it typechecks in ten seconds. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Exponential complexity of type checking (Was: Type-level naturals multiplication)
On Tue, Oct 13, 2009 at 12:32 PM, Serguey Zefirov sergu...@gmail.com wrote: 2009/10/13 Lennart Augustsson lenn...@augustsson.net: Yes, there are simple H-M examples that are exponential. x0 = undefined x1 = (x1,x1) x2 = (x2,x2) x3 = (x3,x3) ... xn will have a type with 2^n type variables so it has size 2^n. Reformulated: let dup x = (x,x) :t dup . dup . dup . dup ... type will be 2^(number of dup's). I experimented and found that GHC can stand pretty long line of dup's. More than 20, at least. One part of our program took too much time to typecheck some time ago. 3 and half minutes for ~900 lines module. Most of operations was inside heavily parametrized monad (5 parameters, each is a Peano number). Then my colleague moved parameters into associated types of relevant type class and now it typechecks in ten seconds. Good example! I have a feeling that the `dup' example is a bit contrived, not something that one would be likely to find in the wild. Heavily parameterized type classes, on the other hand, are more common in real code. Hence, that is more likely where someone would run into really awful type inference performance without expecting it. Brad ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Exponential complexity of type checking (Was: Type-level naturals multiplication)
On Tuesday 13 October 2009 1:06:41 pm Brad Larsen wrote: Good example! I have a feeling that the `dup' example is a bit contrived, not something that one would be likely to find in the wild. This is, after all, why HM is useful. In general, there are programs that take exponential time/space to type check, but those programs don't come up much in real code. Also, you can do better than 2^n: f0 x = (x,x) f1 = f0 . f0 f2 = f1 . f1 f3 = f2 . f2 ... Here, if fN results in a nested tuple of size M, then f(N+1) results in a tuple of size M^2, since we replace all the variables with a copy of the tuple. So we have 2, 4, 16, 256, ... 2^(2^N) Turning f0 into an M-tuple gets you M^(2^N), I believe, and composing K times at each step would get you M^(K^N). But anyhow, we have not merely an exponential, but a double exponential. :) f4 takes a noticeable amount of time to check here (in ghci), and f5 makes my machine start swapping. Of course, one isn't likely to write code like this, either. -- Dan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type checking that I can't figure out ....
Daniel Peebles wrote: Yeah, in a way similar to ArrowPlus/ArrowZero. Then again, I'm not sure whether it would be meaningful to split up MonadPlus like that. Well, we could always have: class MonadZero m = MonadPlus m The suggestion is just to broaden the scope of mzero so that you can have it without requiring mplus as well (since mplus is much more specific than mzero). If we have a MonadZero, then the call to fail when pattern binds fail could be replaced with calls to mzero (or at the very least, fail can be moved to MonadZero as well to clean up Monad). Then Monad is clean and accurate, and people just depend on MonadZero if they choose to do pattern binds rather than catching all patterns with a case expression. -- Live well, ~wren ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type checking that I can't figure out ....
On Wed, Jun 3, 2009 at 8:42 AM, Daniel Fischer daniel.is.fisc...@web.dewrote: Am Mittwoch 03 Juni 2009 06:12:46 schrieb Michael Snoyman: I made two changes: 1. You had the arguments to M.lookup backwards. 2. lookup does not return any generalized Monad, just Maybe (I think that should be changed). Data.Map.lookup used to return a value in any monad you wanted, I believe until 6.8 inclusive. I don't think it's going to change again soon. Is there a reason why it only returns in the Maybe monad? I often times have to write a liftMaybe function to deal with that. Michael ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] type checking that I can't figure out ...
Hi Andrew (Bromage),
I reversed the parameter order to Data.Map.lookup and calling
fromJust to pull out value from Maybe wrapper ... all as you suggested:
remLookupFwd :: (ReVars m t) = SimplRe t - ReM m t (ReInfo t)
remLookupFwd re
= do fwd - gets resFwdMap
let { Just reinfo = fromJust(M.lookup re fwd) }
-- PROBLEM
return reinfo
I am still getting a type mismatch:
Swish\HaskellRDF\Dfa\Dfa.lhs:162:29:
Couldn't match expected type `Maybe t'
against inferred type `ReInfo t1'
In the expression: fromJust (M.lookup re fwd)
In a pattern binding: Just reinfo = fromJust (M.lookup re fwd)
In the expression:
do fwd - gets resFwdMap
let Just reinfo = fromJust (M.lookup re fwd)
return reinfo
Vasili
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type checking that I can't figure out ...
You've applied two solutions to get the value out -- pattern matching
(Just reinfo) and fromJust. You should use one or the other, but not
both:
-- pattern matching
remLookupFwd :: (ReVars m t) = SimplRe t - ReM m t (ReInfo t)
remLookupFwd re
= do fwd - gets resFwdMap
let { Just reinfo = M.lookup re fwd }--
PROBLEM
return reinfo
-- fromJust
remLookupFwd :: (ReVars m t) = SimplRe t - ReM m t (ReInfo t)
remLookupFwd re
= do fwd - gets resFwdMap
let { reinfo = fromJust (M.lookup re
fwd) }-- PROBLEM
return reinfo
BTW, I would personally write this as one line (untested)
gets (fromJust . M.lookup re . resFwdMap)
-Ross
On Jun 3, 2009, at 1:18 PM, Vasili I. Galchin wrote:
Hi Andrew (Bromage),
I reversed the parameter order to Data.Map.lookup and
calling fromJust to pull out value from Maybe wrapper ... all as you
suggested:
remLookupFwd :: (ReVars m t) = SimplRe t - ReM m t (ReInfo t)
remLookupFwd re
= do fwd - gets resFwdMap
let { Just reinfo = fromJust(M.lookup re
fwd) }-- PROBLEM
return reinfo
I am still getting a type mismatch:
Swish\HaskellRDF\Dfa\Dfa.lhs:162:29:
Couldn't match expected type `Maybe t'
against inferred type `ReInfo t1'
In the expression: fromJust (M.lookup re fwd)
In a pattern binding: Just reinfo = fromJust (M.lookup re fwd)
In the expression:
do fwd - gets resFwdMap
let Just reinfo = fromJust (M.lookup re fwd)
return reinfo
Vasili
___
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] type checking that I can't figure out ...
Ross Mellgren schrieb:
You've applied two solutions to get the value out -- pattern matching
(Just reinfo) and fromJust. You should use one or the other, but not both:
-- pattern matching
remLookupFwd :: (ReVars m t) = SimplRe t - ReM m t (ReInfo t)
remLookupFwd re
= do fwd - gets resFwdMap
let { Just reinfo = M.lookup re fwd }-- PROBLEM
return reinfo
-- fromJust
remLookupFwd :: (ReVars m t) = SimplRe t - ReM m t (ReInfo t)
remLookupFwd re
= do fwd - gets resFwdMap
let { reinfo = fromJust (M.lookup re fwd) }
-- PROBLEM
return reinfo
BTW, I would personally write this as one line (untested)
gets (fromJust . M.lookup re . resFwdMap)
fromJust should be avoided, since it is partial and if it results in an
error, the error message points to the implementation of fromJust, not
its application. Pattern matching is better, but 'maybe' and 'fromMaybe'
are best.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type checking that I can't figure out ...
True, so perhaps better written as:
import Data.Maybe (fromMaybe)
gets (fromMaybe (error could not find re in resFwdMap) . M.lookup
re . resFwdMap)
with more detail in error message as appropriate.
-Ross
On Jun 3, 2009, at 5:57 PM, Henning Thielemann wrote:
Ross Mellgren schrieb:
You've applied two solutions to get the value out -- pattern matching
(Just reinfo) and fromJust. You should use one or the other, but
not both:
-- pattern matching
remLookupFwd :: (ReVars m t) = SimplRe t - ReM m t (ReInfo t)
remLookupFwd re
= do fwd - gets resFwdMap
let { Just reinfo = M.lookup re fwd }--
PROBLEM
return reinfo
-- fromJust
remLookupFwd :: (ReVars m t) = SimplRe t - ReM m t (ReInfo t)
remLookupFwd re
= do fwd - gets resFwdMap
let { reinfo = fromJust (M.lookup re fwd) }
-- PROBLEM
return reinfo
BTW, I would personally write this as one line (untested)
gets (fromJust . M.lookup re . resFwdMap)
fromJust should be avoided, since it is partial and if it results in
an
error, the error message points to the implementation of fromJust, not
its application. Pattern matching is better, but 'maybe' and
'fromMaybe'
are best.
___
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] type checking that I can't figure out ....
Michael Snoyman wrote: On Wed, Jun 3, 2009 at 8:42 AM, Daniel Fischer daniel.is.fisc...@web.dewrote: Am Mittwoch 03 Juni 2009 06:12:46 schrieb Michael Snoyman: 2. lookup does not return any generalized Monad, just Maybe (I think that should be changed). Data.Map.lookup used to return a value in any monad you wanted, I believe until 6.8 inclusive. I don't think it's going to change again soon. Is there a reason why it only returns in the Maybe monad? I often times have to write a liftMaybe function to deal with that. Here's the proposal that changed it: http://hackage.haskell.org/trac/ghc/ticket/2309 The discussion about the proposal can be found here: http://www.haskell.org/pipermail/libraries/2008-May/009698.html (There's even the suggestion of adding a function like liftMaybe to Data.Maybe, but apparently nobody turned that into a formal proposal.) Regards, Bertram ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type checking that I can't figure out ....
It seems like if we could get fail out of Monad and into something like MonadFail/Zero, then it might make sense to make a lookup that returned an instance of that instead? Dan On Wed, Jun 3, 2009 at 8:13 PM, Bertram Felgenhauer bertram.felgenha...@googlemail.com wrote: Michael Snoyman wrote: On Wed, Jun 3, 2009 at 8:42 AM, Daniel Fischer daniel.is.fisc...@web.dewrote: Am Mittwoch 03 Juni 2009 06:12:46 schrieb Michael Snoyman: 2. lookup does not return any generalized Monad, just Maybe (I think that should be changed). Data.Map.lookup used to return a value in any monad you wanted, I believe until 6.8 inclusive. I don't think it's going to change again soon. Is there a reason why it only returns in the Maybe monad? I often times have to write a liftMaybe function to deal with that. Here's the proposal that changed it: http://hackage.haskell.org/trac/ghc/ticket/2309 The discussion about the proposal can be found here: http://www.haskell.org/pipermail/libraries/2008-May/009698.html (There's even the suggestion of adding a function like liftMaybe to Data.Maybe, but apparently nobody turned that into a formal proposal.) Regards, Bertram ___ 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] type checking that I can't figure out ....
On Wed, Jun 3, 2009 at 8:52 PM, Daniel Peebles pumpkin...@gmail.com wrote: It seems like if we could get fail out of Monad and into something like MonadFail/Zero, then it might make sense to make a lookup that returned an instance of that instead? Dan Do you mean splitting up MonadPlus/Alternative into two classes? Or we could just return in MonadPlus/Alternative. Antoine ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type checking that I can't figure out ....
Yeah, in a way similar to ArrowPlus/ArrowZero. Then again, I'm not sure whether it would be meaningful to split up MonadPlus like that. On Thu, Jun 4, 2009 at 12:40 AM, Antoine Latter aslat...@gmail.com wrote: On Wed, Jun 3, 2009 at 8:52 PM, Daniel Peebles pumpkin...@gmail.com wrote: It seems like if we could get fail out of Monad and into something like MonadFail/Zero, then it might make sense to make a lookup that returned an instance of that instead? Dan Do you mean splitting up MonadPlus/Alternative into two classes? Or we could just return in MonadPlus/Alternative. Antoine ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] type checking that I can't figure out ....
Hello Haskellers,
I isolated to a not so small piece:
{-# OPTIONS -fglasgow-exts #-}
{-# LANGUAGE UndecidableInstances #-}
import Control.Monad.Identity
import Control.Monad.Reader
import Control.Monad.State
import qualified Data.List as L
import qualified Data.Map as M
import Data.Array
import IOExts
The type of a regular expression.
data Re t
= ReOr [Re t]
| ReCat [Re t]
| ReStar (Re t)
| RePlus (Re t)
| ReOpt (Re t)
| ReTerm [t]
deriving (Show)
The internal type of a regular expression.
type SimplRe t = Int
data SimplRe' t
= SReOr (SimplRe t) (SimplRe t)
| SReCat (SimplRe t) (SimplRe t)
| SReStar (SimplRe t)
| SReLambda
| SReNullSet
| SReTerm t
deriving (Eq, Ord, Show)
The regular expression builder monad.
data (Ord t) = ReRead t
= ReRead {
rerNullSet :: SimplRe t,
rerLambda :: SimplRe t
}
data (Ord t) = ReState t
= ReState {
resFwdMap :: M.Map (SimplRe t) (ReInfo t),
resBwdMap :: M.Map (SimplRe' t) (SimplRe t),
resNext :: Int,
resQueue:: ([SimplRe t], [SimplRe t]),
resStatesDone :: [SimplRe t]
}
type ReM m t a = StateT (ReState t) (ReaderT (ReRead t) m) a
TEMP WNH
Dfa construction
data ReDfaState t
= ReDfaState {
dfaFinal :: Bool,
dfaTrans :: [(t, SimplRe t)]
}
deriving (Show)
TEMP WNH
The ReInfo type
data ReInfo t
= ReInfo {
reiSRE :: SimplRe' t,
reiNullable :: Bool,
reiDfa :: Maybe (ReDfaState t)
}
deriving (Show)
TEMP WNH
class (Monad m, Ord t) = ReVars m t where { }
instance (Monad m, Ord t) = ReVars m t where { }
TEMP WNH
remLookupFwd :: (ReVars m t) = SimplRe t - ReM m t (ReInfo t)
remLookupFwd re
= do fwd - gets resFwdMap
-- let { Just reinfo = M.lookup fwd re }--
PROBLEM
reinfo - M.lookup fwd re -- PROBLEM
return reinfo
When I compile with ghci I get:
Dfa_exp.lhs:91:32:
Couldn't match expected type `M.Map
(M.Map (SimplRe t) (ReInfo t)) t1'
against inferred type `SimplRe t2'
In the second argument of `M.lookup', namely `re'
In a 'do' expression: reinfo - M.lookup fwd re
In the expression:
do fwd - gets resFwdMap
reinfo - M.lookup fwd re
return reinfo
I trimmed the original code down a lot! But still can't why I am getting
type check errors!!! Help!
Kind regards,
Vasili
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type checking that I can't figure out ....
remLookupFwd :: (ReVars m t) = SimplRe t - ReM m t (ReInfo t)
remLookupFwd re
= do fwd - gets resFwdMap
-- let { Just reinfo = M.lookup fwd re }--
PROBLEM
reinfo - liftMaybe $ M.lookup re fwd --
PROBLEM
return reinfo
liftMaybe :: Monad m = Maybe a - m a
liftMaybe Nothing = fail Nothing
liftMaybe (Just x) = return x
I made two changes:
1. You had the arguments to M.lookup backwards.
2. lookup does not return any generalized Monad, just Maybe (I think that
should be changed). I added the simple liftMaybe function to convert the
Maybe result into something that will work with your state monad.
Michael
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type checking that I can't figure out ....
Hi Michael,
Let me look tomorrow morning. In any case, many thanks!
Kind regards,
Vasili
On Tue, Jun 2, 2009 at 11:12 PM, Michael Snoyman mich...@snoyman.comwrote:
remLookupFwd :: (ReVars m t) = SimplRe t - ReM m t (ReInfo t)
remLookupFwd re
= do fwd - gets resFwdMap
-- let { Just reinfo = M.lookup fwd re }--
PROBLEM
reinfo - liftMaybe $ M.lookup re fwd --
PROBLEM
return reinfo
liftMaybe :: Monad m = Maybe a - m a
liftMaybe Nothing = fail Nothing
liftMaybe (Just x) = return x
I made two changes:
1. You had the arguments to M.lookup backwards.
2. lookup does not return any generalized Monad, just Maybe (I think that
should be changed). I added the simple liftMaybe function to convert the
Maybe result into something that will work with your state monad.
Michael
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type checking that I can't figure out ....
G'day Vasili.
This should do it:
remLookupFwd :: (ReVars m t) = SimplRe t - ReM m t (ReInfo t)
remLookupFwd re
= do fwd - gets resFwdMap
let { Just reinfo = fromJust (M.lookup re fwd) }
return reinfo
The FiniteMap lookup operation took its arguments in the opposite order.
That's really the only problem here AFAICT.
Wow, this brings back memories. I wrote this module about ten years ago,
and I'm shocked that it's still getting use. I'd appreciate a copy when
you're done updating it for the modern era.
Cheers,
Andrew Bromage
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type checking that I can't figure out ....
Am Mittwoch 03 Juni 2009 06:12:46 schrieb Michael Snoyman: I made two changes: 1. You had the arguments to M.lookup backwards. 2. lookup does not return any generalized Monad, just Maybe (I think that should be changed). Data.Map.lookup used to return a value in any monad you wanted, I believe until 6.8 inclusive. I don't think it's going to change again soon. I added the simple liftMaybe function to convert the Maybe result into something that will work with your state monad. Michael ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type checking of partial programs
So a number of people responded with various ways this is already possible. Of course GHC can already do this... it's type inference. The part I'm interested in working on is exposing the functionality in GHC's API to make this as easy as possible. -Abram ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type checking of partial programs
On Thu, 20 Mar 2008, Roberto Zunino wrote: ac wrote: foo :: [Foo] - placeholder 1 foo xs = map placeholder 2 xs What are the possible type signatures for placeholder 1 and the possible expressions for placeholder 2? A nice GHCi trick I learned from #haskell: :t let foo xs = map ?placeholder2 xs in foo forall a b. (?placeholder2::a - b) = [a] - [b] Also, the djinn tool might provide some actual expression for placeholder 2. http://www.haskell.org/haskellwiki/Determining_the_type_of_an_expression ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Type checking of partial programs
Is anybody interested in working on this? This is a project I've been interested in for some time, but recognize I probably need some guidance before I go off and start hacking on it. As dcoutts pointed out on #haskell-soc, this may be of particular interest to people working on yi and HaRe. Other interesting and related projects include parsing partial programs to insert placeholders in appropriate places. An example of a partial program could be: foo :: [Foo] - placeholder 1 foo xs = map placeholder 2 xs What are the possible type signatures for placeholder 1 and the possible expressions for placeholder 2? I would like to stir up a discussion about this, and eventually write some useful code. -Abram ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type checking of partial programs
ac wrote: foo :: [Foo] - placeholder 1 foo xs = map placeholder 2 xs What are the possible type signatures for placeholder 1 and the possible expressions for placeholder 2? A nice GHCi trick I learned from #haskell: :t let foo xs = map ?placeholder2 xs in foo forall a b. (?placeholder2::a - b) = [a] - [b] Also, the djinn tool might provide some actual expression for placeholder 2. Zun. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type checking of partial programs
zunino: ac wrote: foo :: [Foo] - placeholder 1 foo xs = map placeholder 2 xs What are the possible type signatures for placeholder 1 and the possible expressions for placeholder 2? A nice GHCi trick I learned from #haskell: :t let foo xs = map ?placeholder2 xs in foo forall a b. (?placeholder2::a - b) = [a] - [b] Also, the djinn tool might provide some actual expression for placeholder 2. Zun. Yes, it turns out implicit parameters provide a great mechanism for doing type checker queries :) -- Don ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type checking of partial programs
You can transform this into valid Haskell98 in the following way: foo_infer xs _ | const False (xs :: [Foo]) = undefined foo_infer xs placeholder_2 = map ph xs foo xs = foo_infer xs undefined You can then do type inference on foo_infer, giving you foo_infer :: [Foo] - (Foo - a) - [a] which gives you the type of the placeholder: placeholder_2 :: Foo - a and the type of foo (which is dependent on that): foo :: [Foo] - [a] Of course this gets far more difficult when you add extensions that require type signatures so that you can't rely entirely on type inference, such as GADTs and higher rank types. But it's a start! -- ryan On 3/20/08, ac [EMAIL PROTECTED] wrote: Is anybody interested in working on this? This is a project I've been interested in for some time, but recognize I probably need some guidance before I go off and start hacking on it. As dcoutts pointed out on #haskell-soc, this may be of particular interest to people working on yi and HaRe. Other interesting and related projects include parsing partial programs to insert placeholders in appropriate places. An example of a partial program could be: foo :: [Foo] - placeholder 1 foo xs = map placeholder 2 xs What are the possible type signatures for placeholder 1 and the possible expressions for placeholder 2? I would like to stir up a discussion about this, and eventually write some useful code. -Abram ___ 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] Type checking with Haskell
Stefan O'Rear wrote: On Thu, Apr 12, 2007 at 01:04:13PM +0100, Joel Reymont wrote: Folks, The ghc/compiler/typecheck directory holds a rather large body of code and quick browsing through did not produce any insight. How do you implement type checking in haskell? Assume I have an Expr type with a constructor per type and functions can take lists of expressions. Do I create a function taking an Expr, pattern-matching on appropriate constructor and returning True on a match and False otherwise? The Glasgow Haskell typechecker is big not because type checking is hard, but because GHC Haskell is a very big language. Also, GHC runs typechecking *before* desugaring, apparently thinking error messages are more important than programmer sanity :) A typechecker for a simpler language can be implemented quite easily: --- Simply typed lambda calculus data Typ = Int | Real | Bool | Fn Typ Typ data Exp = Lam Typ Exp | Var Int | App Exp Exp typeCheck' :: [Typ] - Exp - Maybe Typ typeCheck' cx (Lam ty bd) = fmap (Fn ty) (typeCheck' (ty:cx) bd) typeCheck' cx (Var i) = Just (cx !! i) typeCheck' cx (App fn vl) = do Fn at rt - typeCheck' cx fn pt - typeCheck' cx vl guard (at == pt) return rt Your problem, as I understand it, is even simpler than most since there are no higher order functions and no arguments. --- data Typ = Real | Int | Bool | String tc2 a b ta tb tr | typeCheck a == ta typeCheck b == tb = Just tr | otherwise = Nothing typeCheck :: Exp - Maybe Typ typeCheck (IAdd a b) = tc2 a b Int Int Int ... (That said, it would probably be better to fuse parsing and type checking in this case so that you do not need to track source positions.) Stefan ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe Just for interest: Chapter 31 of Shriram Krishnamurthi's Programming Languages: Application and Interpretation has an interesting perspective on Haskell style polymorphism http://www.cs.brown.edu/~sk/Publications/Books/ProgLangs/ ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Type checking with Haskell
Folks, The ghc/compiler/typecheck directory holds a rather large body of code and quick browsing through did not produce any insight. How do you implement type checking in haskell? Assume I have an Expr type with a constructor per type and functions can take lists of expressions. Do I create a function taking an Expr, pattern-matching on appropriate constructor and returning True on a match and False otherwise? Thanks, Joel -- http://wagerlabs.com/ ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type checking with Haskell
Joel, How do you implement type checking in haskell? You might want to check out Typing Haskell in Haskell [1] by Mark P. Jones. Cheers, Stefan [1] Jones, Mark P. Typing Haskell in Haskell. In Erik Meijer, editor, Proceedings of the 1999 Haskell Workshop, Friday October 9th, 1999, Paris, France. 1999. The proceedings of the workshop have been published as a technical report (UU- CS-1999-28) at Utrecht University. http://www.cs.uu.nl/research/ techreps/UU-CS-1999-28.html ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type checking with Haskell
On Apr 12, 2007, at 1:07 PM, Stefan Holdermans wrote: You might want to check out Typing Haskell in Haskell [1] by Mark P. Jones. Must be _the_ paper as Don suggested it as well. I also looked at my copy of Andrew Appel's compilers in ML book and realized that I should be going about it differently than I thought, i.e. figuring out and returning the type of an expression rather than matching constructors. Oh, well. Thanks, Joel -- http://wagerlabs.com/ ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: [Haskell-cafe] Type checking with Haskell
Hi Joel, You may like to check out my mini-interpreter called (cheekily) baskell: http://www.cs.mu.oz.au/~bjpop/code.html It has type inference, and it is pretty straightforward. I wrote it for teaching purposes. First, I pass over the AST and generate a set of typing constraints. They are just equality constraints. Then I solve the constraints. Couldn't be much simpler than that. Mind you, the input language is pretty minimal (no type classes etcetera). Cheers, Bernie. -Original Message- From: [EMAIL PROTECTED] [mailto:haskell-cafe- [EMAIL PROTECTED] On Behalf Of Joel Reymont Sent: 12 April 2007 13:04 To: Haskell Cafe Subject: [Haskell-cafe] Type checking with Haskell Folks, The ghc/compiler/typecheck directory holds a rather large body of code and quick browsing through did not produce any insight. How do you implement type checking in haskell? Assume I have an Expr type with a constructor per type and functions can take lists of expressions. Do I create a function taking an Expr, pattern-matching on appropriate constructor and returning True on a match and False otherwise? Thanks, Joel -- http://wagerlabs.com/ ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type checking with Haskell
On Thu, Apr 12, 2007 at 01:04:13PM +0100, Joel Reymont wrote: Folks, The ghc/compiler/typecheck directory holds a rather large body of code and quick browsing through did not produce any insight. How do you implement type checking in haskell? Assume I have an Expr type with a constructor per type and functions can take lists of expressions. Do I create a function taking an Expr, pattern-matching on appropriate constructor and returning True on a match and False otherwise? The Glasgow Haskell typechecker is big not because type checking is hard, but because GHC Haskell is a very big language. Also, GHC runs typechecking *before* desugaring, apparently thinking error messages are more important than programmer sanity :) A typechecker for a simpler language can be implemented quite easily: --- Simply typed lambda calculus data Typ = Int | Real | Bool | Fn Typ Typ data Exp = Lam Typ Exp | Var Int | App Exp Exp typeCheck' :: [Typ] - Exp - Maybe Typ typeCheck' cx (Lam ty bd) = fmap (Fn ty) (typeCheck' (ty:cx) bd) typeCheck' cx (Var i) = Just (cx !! i) typeCheck' cx (App fn vl) = do Fn at rt - typeCheck' cx fn pt - typeCheck' cx vl guard (at == pt) return rt Your problem, as I understand it, is even simpler than most since there are no higher order functions and no arguments. --- data Typ = Real | Int | Bool | String tc2 a b ta tb tr | typeCheck a == ta typeCheck b == tb = Just tr | otherwise = Nothing typeCheck :: Exp - Maybe Typ typeCheck (IAdd a b) = tc2 a b Int Int Int ... (That said, it would probably be better to fuse parsing and type checking in this case so that you do not need to track source positions.) Stefan ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type checking with Haskell
Thanks Stefan! On Apr 12, 2007, at 3:00 PM, Stefan O'Rear wrote: Your problem, as I understand it, is even simpler than most since there are no higher order functions and no arguments. I do have functions and arguments but I don't have HOF. (That said, it would probably be better to fuse parsing and type checking in this case so that you do not need to track source positions.) I'm not sure how to do this, quite honestly. The language is dynamically typed so I have to infer variable types from their usage, function return types from what is assigned to the function name (last assignment in program, Fun = xxx). I also have to infer if variables are of a series type by checking if any references are made to the previous values of those variables. I don't think it's possible to fuse type checking with parsing here. -- http://wagerlabs.com/ ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type checking with Haskell
On Apr 12, 2007, at 3:00 PM, Stefan O'Rear wrote: Also, GHC runs typechecking *before* desugaring, apparently thinking error messages are more important than programmer sanity :) What would be the benefit of running type checking after desugaring? -- http://wagerlabs.com/ ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type checking with Haskell
On 4/12/07, Joel Reymont [EMAIL PROTECTED] wrote: What would be the benefit of running type checking after desugaring? After desugaring, the program is written in a much more simple language (GHC Core). Type checking a desugared program is much easier because the type checker has to deal with much less language constructs than in the original program. The disadvantage is that after desugaring a lot of the original program is lost so that the type checker can't give an error message that exactly describes the location and reason of the error. Bas van Dijk ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type checking with Haskell
It's so much easier to write the type checker because it's only a few constructs left in the language. But from a user's perspective it's a really bad idea. -- Lennart On Apr 12, 2007, at 15:25 , Joel Reymont wrote: On Apr 12, 2007, at 3:00 PM, Stefan O'Rear wrote: Also, GHC runs typechecking *before* desugaring, apparently thinking error messages are more important than programmer sanity :) What would be the benefit of running type checking after desugaring? -- http://wagerlabs.com/ ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Type checking and locating token with Parsec
Folks, Imagine a language where Num + Num yields a Num and Str + Num yields a Str but Num + Str should not be allowed. I implemented parsing for such a language in OCaml with a yacc-based parser without an additional type-checking pass, entirely within the yacc grammar. I tried to take such an approach with Parsec but hit the roadblock with buildExpressionParser since it returns the same type as the token parser given to it. Rather than have numerical expressions, string expressions, etc., as separate types, I simplified things down to a single expression type that holds my booleans, strings and numbers. I now need to implement type checking of my parsed AST. The main issue is error reporting. I'm not sure where to get token location with Parsec and how to elegantly embed it in my AST. Has anyone implemented type checking on top of a Parsec-based parser? How did you locate your tokens? Thanks, Joel -- http://wagerlabs.com/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type checking and locating token with Parsec
On Tue, Apr 10, 2007 at 02:09:03PM +0100, Joel Reymont wrote: Folks, Imagine a language where Num + Num yields a Num and Str + Num yields a Str but Num + Str should not be allowed. I implemented parsing for such a language in OCaml with a yacc-based parser without an additional type-checking pass, entirely within the yacc grammar. I tried to take such an approach with Parsec but hit the roadblock with buildExpressionParser since it returns the same type as the token parser given to it. Just because you have a hammer doesn't mean you have a nail. I've gotten along all this time never learning buildExpressionParser, instead hand-coding my precedence parsers. Rather than have numerical expressions, string expressions, etc., as separate types, I simplified things down to a single expression type that holds my booleans, strings and numbers. I now need to implement type checking of my parsed AST. Would something like this work for you: data NumExpr = ... data StrExpr = ... data Expr = NumExpr NumExpr | StrExpr StrExpr addExpr :: Expr - Expr - CharParser st Expr addExpr (NumExpr n) (NumExpr m) = NumExpr (Add n m) addExpr (StrExpr n) (NumExpr m) = StrExpr (Cat n (ToString m)) ... op3 ch fn a b = join $ liftM3 (\x _ y - fn x y) a (char ch) b ... exp0 = op3 '+' addExpr exp1 exp0 ... It might also be good to modify chainl1/chainr1, with support for possibly failing operations. Remember - the provided abstractions have failed you, but you can still define your own! The main issue is error reporting. I'm not sure where to get token location with Parsec and how to elegantly embed it in my AST. Has anyone implemented type checking on top of a Parsec-based parser? How did you locate your tokens? There's haskell-src: http://haskell.org/ghc/dist/current/docs/libraries/haskell-src/Language-Haskell-Syntax.html And people wonder why I decided to abuse template haskell instead of using the standard AST type. You do NOT want to go there. Not until Oleg invents a way to make this stuff automatic, anyway. Stefan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] powerful type checking false expectations that a program is correct
Programmers who use languages without static type checking sometimes claim that static type checking gives folk the false impression that once the program passes type checking the program is correct. That always seemed silly to me, but I'm starting to wonder ;-) Of course, the shootout programs are a silly entertainment; but after taking the time to optimise and write the programs, I'm a little surprised that there have been Haskell contributions which just don't give 'the correct answer' in a way that visual inspection with the expected answer would detect. For example ackermann Haskell GHC program regex-dna (new) Haskell GHC #2 program Oh well, they are just easy to fix formating bugs :-) __ Do You Yahoo!? Tired of spam? Yahoo! Mail has the best spam protection around http://mail.yahoo.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Problem type checking class-method implementation
Dear Haskellers,
Yesterday I stumbled upon a problem type checking a program involving
multi-parameter type classes. GHC rejected the program; still, I was
not immediately convinced it contained a type error. Having given it
some more thoughts, I start to suspect that the type checker is in err
and that the program is well-typed after all. But, well, I might be
overlooking something obvious...
I have reduced my code to a small but hopelessly contrived example
program exposing the problem. Please hang on.
Because we employ multi-parameter type classes, we need the Glasgow
extensions:
{-# OPTIONS -fglasgow-exts #-}
Let's start easy and define the identity monad:
newtype Identity a = Identity {runIdentity :: a}
instance Monad Identity where
return = Identity
Identity a = f = f a
Then, let's introduce the foundations for the (contrived) example:
class (Monad m) = IsItem m i where
processItem :: i - m ()
class (Monad m) = IsProcessor p m | m - p where
process :: (IsItem m i) = i - m ()
-- ...some more methods, possibly involving p...
So, an item is something that can be processed within the context of a
certain monad, and a processor is something that can process an item of
an appropriate type. Note the functional dependency from m to p: a
processor type m uniquely determines the type of the processing context
p.
Before we move on, consider this canonical item type, which is just a
one-field record representing an implementation of the IsItem class:
newtype Item m = Item {processItemImpl :: m ()}
The corresponding instance declaration is obvious:
instance (Monad m) = IsItem m (Item m) where
processItem = processItemImpl
Furthermore values of every type that is an instance of IsItem can be
converted to corresponding Item values:
toItem :: (IsItem m i) = i - Item m
toItem = Item . processItem
Please stick with me, for we are now going to implement a monad
transformer for processors (which, for this example, is really just the
identity monad transformer):
newtype ProcessorT p m a = ProcessorT {runProcessorT :: m a}
instance (Monad m) = Monad (ProcessorT p m) where
return = ProcessorT . return
ProcessorT m = f = ProcessorT (m = runProcessorT . f)
instance (Monad m) = IsProcessor p (ProcessorT p m) where
process = processItem
Then, finally, we use this transformer to derive a processor monad:
newtype Processor p a = Processor {unwrap :: ProcessorT p Identity a}
runProcessor :: Processor p a - a
runProcessor = runIdentity . runProcessorT . unwrap
So, we just make sure that Processor is a monad:
instance Monad (Processor p) where
return= Processor . return
Processor m = f = Processor (m = unwrap . f)
Now all what is left to do is declare Processor an instance of
IsProcessor. To this end, we need to be able to cast items for
Processor p to items for ProcessorT p Identity (for all p). The
following function takes care of that:
castItem :: (IsItem (Processor p) i) = i - Item (ProcessorT p
Identity)
castItem = Item . unwrap . processItem
Note that up 'til now everything is fine: GHC is happy, I am happy. But
then,
when all the hard work is done, and we just only have to connect things
properly, it just breaks:
instance IsProcessor p (Processor p) where
process = Processor . process . castItem
After adding this last instance declaration, GHC happily reports:
Processor.hs:56:24:
Could not deduce (IsItem (ProcessorT p Identity)
(Item (ProcessorT p1 Identity)))
from the context (IsProcessor p (Processor p),
Monad (Processor p),
IsItem (Processor p) i)
arising from use of `process' at Processor.hs:56:24-30
Probable fix:
add (IsItem (ProcessorT p Identity) (Item (ProcessorT p1
Identity)))
to the class or instance method `process'
or add an instance declaration for
(IsItem (ProcessorT p Identity)
(Item (ProcessorT p1 Identity)))
In the first argument of `(.)', namely `process'
In the second argument of `(.)', namely `process . castItem'
In the definition of `process': process = Processor . (process .
castItem)
Processor.hs:56:34:
Could not deduce (IsItem (Processor p1) i)
from the context (IsProcessor p (Processor p),
Monad (Processor p),
IsItem (Processor p) i)
arising from use of `castItem' at Processor.hs:56:34-41
Probable fix:
add (IsItem (Processor p1) i) to the class or instance method
`process'
or add an instance declaration for (IsItem (Processor p1) i)
In the second argument of `(.)', namely `castItem'
In the second argument of `(.)', namely `process . castItem'
In the definition of `process': process = Processor . (process .
castItem)
It seems to me that the type checker fails
RE: [Haskell-cafe] Problem type checking class-method implementation
Stefan,
the problem can be spotted in the following erased version of your
program.
data Identity a
instance Monad Identity
class (Monad m) = IsItem m i where
processItem :: i - m ()
class (Monad m) = IsProcessor p m | m - p where
process :: (IsItem m i) = i - m ()
newtype Item m = Item {processItemImpl :: m ()}
newtype ProcessorT p m a = ProcessorT {runProcessorT :: m a}
instance (Monad m) = Monad (ProcessorT p m)
instance (Monad m) = IsProcessor p (ProcessorT p m)
newtype Processor p a = Processor {unwrap :: ProcessorT p Identity a}
instance Monad (Processor p) where
castItem :: (IsItem (Processor p) i) = i - Item (ProcessorT p
Identity)
castItem = undefined
instance IsProcessor p (Processor p) where
process = Processor . process . castItem
Recall the type error:
Could not deduce (IsItem (Processor p1) i)
from the context (IsProcessor p (Processor p),
Monad (Processor p),
IsItem (Processor p) i)
The problem is basically in here:
instance IsProcessor p (Processor p) where
process = Processor . process . castItem
By specializing function signatures according to the instance head,
and by applying type checking constraints for functional composition,
we get these types:
Processor :: ProcessorT p Identity () - Processor p ()
process :: process :: ( IsProcessor p (ProcessorT p Identity)
, IsItem (ProcessorT p1 Identity) ()
)
= Item (ProcessorT p1 Identity)
- ProcessorT p Identity ()
castItem :: (IsItem (Processor p1) i) =
i - Item (ProcessorT p1 Identity)
The problem is the type-scheme polymorphic result type of
castItem which is consumed by a type-variable polymorphic
but type-class bounded argument type of process.
The constraint of this application process, i.e.,
IsItem (Processor p1) i
is the one GHC asks for.
(Do the hugs test :-))
Ralf
-Original Message-
From: [EMAIL PROTECTED] [mailto:haskell-cafe-
[EMAIL PROTECTED] On Behalf Of Stefan Holdermans
Sent: Wednesday, August 03, 2005 1:01 AM
To: haskell-cafe
Subject: [Haskell-cafe] Problem type checking class-method
implementation
Dear Haskellers,
Yesterday I stumbled upon a problem type checking a program involving
multi-parameter type classes. GHC rejected the program; still, I was
not immediately convinced it contained a type error. Having given it
some more thoughts, I start to suspect that the type checker is in err
and that the program is well-typed after all. But, well, I might be
overlooking something obvious...
I have reduced my code to a small but hopelessly contrived example
program exposing the problem. Please hang on.
Because we employ multi-parameter type classes, we need the Glasgow
extensions:
{-# OPTIONS -fglasgow-exts #-}
Let's start easy and define the identity monad:
newtype Identity a = Identity {runIdentity :: a}
instance Monad Identity where
return = Identity
Identity a = f = f a
Then, let's introduce the foundations for the (contrived) example:
class (Monad m) = IsItem m i where
processItem :: i - m ()
class (Monad m) = IsProcessor p m | m - p where
process :: (IsItem m i) = i - m ()
-- ...some more methods, possibly involving p...
So, an item is something that can be processed within the context of a
certain monad, and a processor is something that can process an item
of
an appropriate type. Note the functional dependency from m to p: a
processor type m uniquely determines the type of the processing
context
p.
Before we move on, consider this canonical item type, which is just a
one-field record representing an implementation of the IsItem class:
newtype Item m = Item {processItemImpl :: m ()}
The corresponding instance declaration is obvious:
instance (Monad m) = IsItem m (Item m) where
processItem = processItemImpl
Furthermore values of every type that is an instance of IsItem can be
converted to corresponding Item values:
toItem :: (IsItem m i) = i - Item m
toItem = Item . processItem
Please stick with me, for we are now going to implement a monad
transformer for processors (which, for this example, is really just
the
identity monad transformer):
newtype ProcessorT p m a = ProcessorT {runProcessorT :: m a}
instance (Monad m) = Monad (ProcessorT p m) where
return = ProcessorT . return
ProcessorT m = f = ProcessorT (m = runProcessorT . f)
instance (Monad m) = IsProcessor p (ProcessorT p m) where
process = processItem
Then, finally, we use this transformer to derive a processor monad:
newtype Processor p a = Processor {unwrap :: ProcessorT p Identity
a}
runProcessor :: Processor p a - a
runProcessor = runIdentity . runProcessorT . unwrap
So, we just make sure that Processor is a monad:
instance Monad (Processor p) where
return
Re: [Haskell-cafe] Problem type checking class-method implementation
Ralf, The problem is the type-scheme polymorphic result type of castItem which is consumed by a type-variable polymorphic but type-class bounded argument type of process. Thanks for your explanation: I hope it's still safe to say that I did not miss something entirely obvious. :) Anyway, indeed, I do see bubbling that one type-class constraint to the top-level. So, playing around, rewriting things just a little, I end up with instance IsProcessor p (Processor p) where process = Processor . unwrap . processItem which is disappointingly the most obvious implementation anyway. Disappointingly, however, because it equivalent to what I had written in the original program, i.e., the one that brought me to consider all this in the first place. And there, for some reason, it did not work and led me to the deviation via (something equivalent to) castItem. Well, that's what you get from simplifying stuff. Anyway, it seems time to have another look at the original program and maybe come with another type-checking puzzle later. ;) Thanks, Stefan http://www.cs.uu.nl/~stefan/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Type checking
Hi, Can anyone explain to me how hugs manages to derive that f x y z = y (y z) x is of type f :: a - ((a - b) - a - b) - (a - b) - b This question was posted from an Oxford University computer; it also smells like homework. If it's genuinely not homework, Lee, I apologise! See http://www.haskell.org/hawiki/HomeworkHelp --KW 8-) -- Keith Wansbrough [EMAIL PROTECTED] http://www.cl.cam.ac.uk/users/kw217/ University of Cambridge Computer Laboratory. ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Type checking
Hi, Can anyone explain to me how hugs manages to derive that f x y z = y (y z) x is of type f :: a - ((a - b) - a - b) - (a - b) - b Many thanks and a happy new year to all! Lee _ Stay in touch with absent friends - get MSN Messenger http://www.msn.co.uk/messenger ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Type checking
On 2003-12-31 at 19:27GMT Lee Dixon wrote: Hi, Can anyone explain to me how hugs manages to derive that f x y z = y (y z) x is of type f :: a - ((a - b) - a - b) - (a - b) - b To begin with, f has three arguments, x y and z, so letting each of these have types Tx Ty and Tz, f has to have type Tx - Ty - Tz - R, for some R. We see that y is applied to z, so y must have type Tz - Ry: f:: Tx - (Tz - Ry) - Tz - R but y is also applied to (y z) and x. (y z):: Ry, so y must also have type Ry - Tx - R since R is the type of the body of f. so we need to find a type that has instances Tz - Ry and Ry - Tx - R putting Ry = (a - b), we want Tz - (a - b) to be the same as (a - b) - Tx - R, which it is if Tz = (a - b), Tx = a and R = b. ie Ty = (a - b) - a - b. So substitute all those in the first guess for the type of f we get a - ((a - b) - a - b) - (a - b) - b | ---|------|| |Tz Tz | |-|--| TxTy R You want to look up unification and Hindley-Milner type inference. Does that help? Jón -- Jón Fairbairn [EMAIL PROTECTED] ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Type checking/inference
Hi, prelude :t map (foldr filter) map (foldr filter) :: [[a]] - [[a - Bool] - [a]] Two main questions: 1/ How does hugs derive this answer? 2/ What input can I give so that it yields a correct result? I've tried giving it a list of lists but it fails... Try: map (flip (foldr filter) [even,odd]) [[1,2,3],[4,5,6]] I guess this meets your expectation. Without flipping the arguments: Prelude map (foldr filter [1,2,3]) [[even]] [[2]] Prelude map (foldr filter [1,2,3]) [[even],[even,odd]] [[2],[]] Prelude map (foldr filter [1,2,3]) [[even],[even,odd],[odd]] Bye, Steffen ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Type checking/inference
Lee Dixon wrote: I've run into a small problem whilst doing some manual type checking, to see if I could match the results given by hugs prelude :t foldr filter foldr filter :: [a] - [a - Bool] - [a] -- This was fine and was the same as my answer, so I tested it with prelude foldr filter [1,2,3,4] [even,odd] -- and the answer was indeed an empty list -- However I got stuck when attempting to derive the result of map (foldr filter) -- Hugs says that: prelude :t map (foldr filter) map (foldr filter) :: [[a]] - [[a - Bool] - [a]] Two main questions: 1/ How does hugs derive this answer? filter :: (a - Bool) - [a] - [a] foldr:: (a - b - b) - b - [a] - b map :: (a - b) - [a] - [b] Passing filter as the argument to foldr instantiates a as (a - Bool) and b as [a], giving: foldr filter :: [a] - [a - Bool] - [a] Passing (foldr filter) as the argument to map instantiates a as [a] and b as ([a - Bool] - [a]), giving: map (foldr filter) :: [[a]] - [[a - Bool] - [a]] 2/ What input can I give so that it yields a correct result? I've tried giving it a list of lists but it fails... The return value is a list of functions, and functions aren't instances of Show, so it can't print the result. Maybe you didn't mean (map (foldr filter))? The argument to map is usually a function of one argument (i.e. a function whose result *isn't* a function). What are you ultimately trying to achieve? -- Glynn Clements [EMAIL PROTECTED] ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Type checking/inference
On Sun, 28 Dec 2003 04:58:12 + Lee Dixon [EMAIL PROTECTED] wrote: Hi, I've run into a small problem whilst doing some manual type checking, to see if I could match the results given by hugs prelude :t foldr filter foldr filter :: [a] - [a - Bool] - [a] -- This was fine and was the same as my answer, so I tested it with prelude foldr filter [1,2,3,4] [even,odd] -- and the answer was indeed an empty list -- However I got stuck when attempting to derive the result of map (foldr filter) -- Hugs says that: prelude :t map (foldr filter) map (foldr filter) :: [[a]] - [[a - Bool] - [a]] Two main questions: 1/ How does hugs derive this answer? map :: (a - b) - [a] - [b] foldr filter :: a' - b' where a' = [a] and b' = [a - Bool] - [a] map (foldr filter) :: [a'] - [b'] where a' = [a] and b' = [a - Bool] - [a] so map (foldr filter) :: [[a]] - [[a - Bool] - [a]] 2/ What input can I give so that it yields a correct result? Typewise, it is the correct result for what you've provided. Typewise or termwise, what do you want the result to be? I've tried giving it a list of lists but it fails... What does 'fails' mean? Type error, run-time error, wrong output ... ? What is the input? What is the expected output? What is the text of the output (error message, actual output, etc.)? Right now, all people can do is take guesses at what you want. ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Type checking/inference
Hi, I've run into a small problem whilst doing some manual type checking, to see if I could match the results given by hugs prelude :t foldr filter foldr filter :: [a] - [a - Bool] - [a] -- This was fine and was the same as my answer, so I tested it with prelude foldr filter [1,2,3,4] [even,odd] -- and the answer was indeed an empty list -- However I got stuck when attempting to derive the result of map (foldr filter) -- Hugs says that: prelude :t map (foldr filter) map (foldr filter) :: [[a]] - [[a - Bool] - [a]] Two main questions: 1/ How does hugs derive this answer? 2/ What input can I give so that it yields a correct result? I've tried giving it a list of lists but it fails... Any pointers would be greatly appreciated! Many Thanks, Lee _ Stay in touch with absent friends - get MSN Messenger http://www.msn.co.uk/messenger ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
