Re: API function to check whether one type fits "in" another
Dear Simon, et al, Thank you very much for your reply. Some of the pointers you gave, I wouldn't have come across, for not knowing to have to browse through the module Inst, for example. I read the OutsideIn paper (JFP), but that's a fair while back. I was pointed to Thijs's work in progress at an Agda talk recently. The front-end we're working on should be portable to any lambda-language with strong types, so the availability of holes in Agda and Idris makes the implementation for those back-ends a breeze. There is one limiting consideration, however: We want to get this up and running the next few weeks and we would like to keep things in-sync with the developments on the different back-ends. This is why I'm trying to stay as close as possible to the more "public" API parts (the things that are documented and haven't changed significantly since at least 7.0.4). In this light, I was wondering whether it's not worth having a function that does all this plumbing in the API that is persistent through future versions, much like pure interface to the parser (GHC.parser). Preferably it would look something like: typeCheck :: DynFlags -- the flags -> FilePath -- for source locations -> Type -- expected -> Type -- actual -> Either SomeSortOfErrorStructure SomeSubstitutionAndOrConstraintTable The implementation would have to make sure the pre-conditions of the type arguments are met. Is this worth pursuing? Would be a significant amount of work? Am I being pushy if I make this a feature-request? Regards, Philip PS. I'm going to study the Trac you pointed to in more detail; browsing it was already a learning experience about the whats and wheres of the GHC API. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: API function to check whether one type fits "in" another
L.S., I've come up with some minor progress myself, but I could still do with a little help. The attached file is the smallest thing I could come up with to replicate my problem. I'm using tcMatchTy now to try and match two types, hoping to find TyVar substitutions when the types unify. Given the functions in the attached file and the ghci-session below this message (from the current Haskell Platform), could anyone explain the misses (the ones that result in Nothing)?? Regards, Philip P.S. Note that type variables are pretty printed to simply 'a' or 'b'. The names are disambiguated only locally, so in the trace below, not every 'a' is equal to every other 'a' (but this becomes obvious from the corresponding InScopeSet) Ghci session: *CheckType> matchHole "fmap" 0 "id" Hole: FunTy (TyVarTy a) (TyVarTy b) Term: FunTy (TyVarTy a) (TyVarTy a) Vars: [a,b,a] Just (TvSubst InScopeSet [(a15M9,a),(a15Ma,b),(a15Mg,a)] [(a15M9,TyVarTy a),(a15Ma,TyVarTy a)]) *CheckType> matchHole "fmap" 0 "(+)" Hole: FunTy (TyVarTy a) (TyVarTy b) Term: FunTy (TyConApp GHC.Num.Num [TyVarTy a]) (FunTy (TyVarTy a) (FunTy (TyVarTy a) (TyVarTy a))) Vars: [a,b,a] Nothing *CheckType> matchHole "(+)" 0 "0" Hole: FunTy (TyConApp GHC.Num.Num [TyVarTy a]) (TyVarTy a) Term: FunTy (TyConApp GHC.Num.Num [TyVarTy a]) (TyVarTy a) Vars: [a,a] Just (TvSubst InScopeSet [(a168l,a),(a168s,a)] [(a168l,TyVarTy a)]) *CheckType> matchHole "fmap" 1 "[True]" Hole: FunTy (TyConApp GHC.Base.Functor [TyVarTy f]) (AppTy (TyVarTy f) (TyVarTy a)) Term: TyConApp [] [TyConApp GHC.Types.Bool []] Vars: [f,a] Nothing *CheckType> matchHole "map" 1 "[True]" Hole: TyConApp [] [TyVarTy a] Term: TyConApp [] [TyConApp GHC.Types.Bool []] Vars: [a] Just (TvSubst InScopeSet [(adpV,a)] [(adpV,TyConApp GHC.Types.Bool [])]) *CheckType> CheckType.hs Description: Binary data ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
API function to check whether one type fits "in" another
L.S., I sent this to the cvs-ghc list, but was - correctly - redirected here. We're trying to write an alternative interactive front-end (alternative to ghci). This front-end is very type-driven; terms are composed not as characters on a prompt, but as applications of terms to terms. At every application of a term to another, we want to check whether the application is well typed and what type variables would have to change. Suppose I want to build the term flip fmap (+) :: Num n => ((n -> n) -> b) -> n -> b In our front-end, however, we do not need the flip; we leave unfilled holes with their type annotated, so the above would really look like this (where [[ and ]] denote a hole): fmap [[ (n -> n) -> b ]] (+) :: Num n => n -> b We start this off by asking for the types of these separate things, using GHC.exprType, giving: fmap: ForAllTy f (ForAllTy a (ForAllTy b (FunTy (TyConApp GHC.Base.Functor [TyVarTy f]) (FunTy (FunTy (TyVarTy a) (TyVarTy b)) (FunTy (AppTy (TyVarTy f) (TyVarTy a)) (AppTy (TyVarTy f) (TyVarTy b))) (+): ForAllTy a (FunTy (TyConApp GHC.Num.Num [TyVarTy a]) (FunTy (TyVarTy a) (FunTy (TyVarTy a) (TyVarTy a (Note that 'Var' things are pretty printed to just show their name, whereas all the constructors of Type are displayed using show.) The thing that we really want to ask the GHC-API is whether (+) 'fits into' the second argument-hole of fmap, i.e. we want to know whether (type of +) ForAllTy a (FunTy (TyConApp GHC.Num.Num [TyVarTy a]) (FunTy (TyVarTy a) (FunTy (TyVarTy a) (TyVarTy a fits into (type of second argument of fmap) ForAllTy f (ForAllTy a (FunTy (TyConApp GHC.Base.Functor [TyVarTy f]) (AppTy (TyVarTy f) (TyVarTy a What I'm looking for is a function fitsInto :: TermType -> HoleType -> Maybe [(TyVar,Type)] I have found many functions in TcUnify / Unify / TcMatches that look somewhat like this, but in all cases they required extra arguments. When these extra arguments are filled with arbitrary values, the result is always Nothing or some sort of panic. Any pointers would be truly welcome. Regards, Philip ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: ANNOUNCE: GHC version 6.8.1
Dear Ian, Duncan, all, Thank you for looking into the build failure. I actually expected that the autoconf warning didn't really matter, since I couldn't imagine any ReiserFS dependency being critical. The other error is actually quite a lot more weird and critical, for it stops the build. Regards, Philip ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Little help with length bounded lists (Addendum)
PS.
This program requires:
{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
PPS.
Sorry for the extra mail
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Little help with length bounded lists
Dear GHC-ers, I'm trying to write a program using list-length codings in types. Based on the material from the many "faking it" papers I've found, I wrote up the following class, where 'l' is the list type, 'a' is the type of the elements in the list and 'n' is the number of elements in the list: class BoundList l a n | l -> a n where asList :: l -> [a] llength :: l -> n mkList :: [a] -> (l,[a]) Now I made two obvious list-constructors WITH the corresponding type constructors: data Nil a = Nil data Cons a n tl = Cons a tl Empty lists are typed with the parameter of the type constructor. Non-empty lists are typed, but by using only the definition above, the list may be heterogeneous (there are no restrictions on tl). By making these types instances of the BoundList class, lists are homogeneous (see below). Lengths are coded linearly as: data Z -- zero data S x -- successor Giving the means to restrict the length of lists as well. The instance declarations look like this: instance BoundList (Nil a) a Z where asList _= [] llength _= (undefined :: Z) mkList as = (Nil, as) instance BoundList l a n => BoundList (Cons a (S n) l) a (S n) where asList (Cons a as) = a : asList as llength _ = (undefined :: S n) mkList (a:as) = (Cons a tl, rs) where (tl,rs) = mkList as Based on Uktaad B'mal's "Beginning Faking It" paper, I constructed reflection and reification of the length coding, viz: class Reflect s where intValue :: s -> Int instance Reflect Z where intValue _ = 0 instance Reflect x => Reflect (S x) where intValue _ = intValue (undefined :: x) + 1 reifyInt :: Int -> (forall s . Reflect s => s -> w) -> w reifyInt 0 k = k (undefined :: Z) reifyInt (n+1) k = reifyInt n (\(_::s) -> k (undefined :: S s)) What I can't bend my mind around, is how I should construct a function that will partition a normal list into a list of length bounded lists. Basically, I want to have a function that, given an Int n and a list list xs, that chops up xs into chunks of size n and actually constructs Cons/Nil lists for me. I understand that I can't "bring the type out," as in: partition :: BoundList l a n => Int -> [a] -> l but I would have hoped for a way to apply functions to my constructed bounded lists, like, maybe: partition :: Int -> [a] -> (forall l . BoundList l a n => l -> w) -> [w] Like I said, my mind doesn't bend this way. Does anybody have a suggestion that can help me out? Also, have I blatantly missed a library that will neatly do this for me? Eventually, I want to use this library so that I can define a block size in my function types. This could (hopefully) be used to do SDF-like run-time scheduling of threads, or - when distributed over multiple processors - processes. Regards, Philip ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Why only inference in type checking?
Dear Simon, You mentioned that GHC uses 'checking' when it knows the types. How this relates to 'unification', I don't know. It might very well be the same. Hopefully, the following example sheds a bit more light on what I mean (carefully nicked from Uktaad B'mal's "Beginning Faking It"). Examples are many, including in the "Understanding FDs via CHRs" paper. -- Start example To define 'vectors,' we need to code the length of a list in a type. With the zero/successor notation for naturals, we can do this is data constructors without term-level constructors: data Z data S x Vector concatenation requires addition of these numerals. In Prolog terms: Add(zero, X, X). Add(s X, Y, s Z) :- Add X Y Z We can translate this to a type class as class Add a b c | a b -> c instance Add Z x x instance Add x y z => Add (S x) y (S z) -- End example Because of your paper I understand why the coverage condition is in place and why it fails for the last of these instance declarations. GHC will allow me to do this by saying allow-undecidable-instances. As you state in the paper, the three FD-conditions of Coverage, Consistency and Bound Variable are sufficient, but not (always) necessary. I see why the example above causes considerable problems for inference, but if I read these instance declarations as Horn clauses, I see no problem at all in checking any actual occurrence in a program, i.e. if I write a concatenation function for vectors that uses this class as a property of vectors, I don't see where a type checker, using Prolog-like unification, runs into difficulties. What I'm probably asking (it's hard to tell, even for me, sometimes), is whether there is something between a type checker that is guaranteed to terminate and throwing all guarantees with regards to decidability right out the window. Again, I might be completely mistaken about how GHC does this. In that case I would like to find out where I make a wrongful assumption. Regards, Philip ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Why only inference in type checking?
Dear All, A while ago, I had trouble understanding the coverage condition and I raised a question on this mailing list. Help was swift and adequate, especially the reference to the paper entitled "Understanding Functional Dependencies via Constraint Handling Rules" was very useful. However, having considered the problem of non-termination of the type checker, I can't help but wonder why the type checker is "inference only." From the paper mentioned above, consider the following example: class Mul a b c | a b -> c where (*) :: a -> b -> c type Vec b = [b] instance Mul a b c => Mul a (Vec b) (Vec c) where ... f b x y = if b then (*) x [y] else y For actual arguments of f, there is no issue whatsoever with decidability. The type checker in my brain uses unification, i.e. top-down. The type checker in GHC uses inference, i.e. bottom-up. Why inference potentially suffers from non-termination for this program, I understand. My question is this: Is there a reason why type checking in GHC is inference-only, as opposed to a meet-in-the-middle combination of unification and inference? Would the type checker use both unification and inference (let's say alternating evaluation of both), the number of programs for which termination can be guaranteed is considerably larger - if I'm not mistaken, but I may very well have gotten it wrong. Regards, Philip PS. I realize that for this dependent typing scenario is useless once Type Families are here. I can't wait for a GHC with TFs. I raise this question, simply to understand why inference was chosen exclusively. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: ANNOUNCE: GHC 6.8.1 Release Candidate
Dear Ian, all, I'm getting a build error that I've seen before. I must be overlooking something. What I do: [EMAIL PROTECTED]:~/local/src> curl http://www.haskell.org/ghc/dist/stable/dist/ghc-6.8.20070912-src.tar.bz2 | tar -xj % Total% Received % Xferd Average Speed TimeTime Time % Current Dload Upload Total SpentLeft Speed 100 6893k 100 6893k0 0 682k 0 0:00:10 0:00:10 --:--:-- 743k [EMAIL PROTECTED]:~/local/src> cd ghc-6.8.20070912 [EMAIL PROTECTED]:~/local/src/ghc-6.8.20070912> ./boot Booting . Booting libraries/base Booting libraries/directory /usr/share/aclocal/progsreiserfs.m4:13: warning: underquoted definition of AC_CHECK_LIBREISERFS run info '(automake)Extending aclocal' or see http://sources.redhat.com/automake/automake.html#Extending-aclocal Booting libraries/old-time Booting libraries/process Booting libraries/readline Booting libraries/unix [EMAIL PROTECTED]:~/local/src/ghc-6.8.20070912> ./configure && make [...] make[1]: *** No rule to make target `../includes/DerivedConstants.h', needed by `stage1/codeGen/CgProf.o'. Stop. make[1]: Leaving directory `/local/holzensp/src/ghc-6.8.20070912/compiler' make: *** [stage1] Error 1 Either this is a bugreport or a kind request for advice. Regards, Philip ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Need help understanding the Coverage Condition
On Wed, Jul 04, 2007 at 05:35:44PM +0100, Simon Peyton-Jones wrote: > Have you read "Understanding functional dependencies via Constraint > Handling Rules"? > http://research.microsoft.com/~simonpj/papers/fd-chr > > If not, I urge you to consider doing so. It goes into the whole > thing in great detail. I'm submerged for the next 3 weeks, though > others may be able to help you. Simon, I knew I had a "to read" scribbled down in the back of my mind somewhere, but it had slipped out. I will read that paper and see how far I get (although it still seems that it should be possible to relax the covering condition somewhat, being that the example I gave is decidable on paper ;) ) Thank you for the reference. Regards, Philip ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Need help understanding the Coverage Condition
L.S.,
I have difficulty understanding the Coverage Condition. Hopefully,
someone has the time and is willing to explain this to me. Obviously,
I went ahead and hacked together something horribly entangled, but I
found a small example that already shows the behaviour I do not
understand.
Type-level addition of Church numerals:
{- begin -}
{-# OPTIONS -fglasgow-exts #-}
data Z-- Zero
data S x -- Successor of x
class Add a b c | a b -> c
instance Add Z q q
instance Add p q r => (S p) q (S r)
{- end -}
The error GHCi produces is:
Illegal instance declaration for `Add (S x) y (S z)'
(the Coverage Condition fails for one of the functional
dependencies;
Use -fallow-undecidable-instances to permit this)
In the instance declaration for `Add (S x) y (S z)'
Failed, modules loaded: none.
I checked the user guide (7.4.4.1) for criteria for functional
dependencies and checked that I do not violate the assertions. I don't
violate assertions 1a and 1b, but assertion 2 (the coverage condition)
I have trouble reading:
The coverage condition. For each functional dependency, tvc_left ->
tvs_right, of the class, every type variable in S(tvs_right) must
appear in S(tvs_left), where S is the substitution mapping each type
variable in the class declaration to the corresponding type in the
instance declaration.
In my mind, in this case:
tvs_left = {a,b}
tvs_right= {c}
S(tvs_left) = {p,q}
S(tvs_right) = {r}
What "occur in" means (mappings of type variables occurring in
mappings of other type variables), I really don't quite understand.
The example in the manual under 7.4.4.2, viz:
instance Mul a b c => Mul a [b] [c] where x .*. v = map (x.*.) v
seams related, but unfortunately is not elaborated upon beyond "[it]
does not obey the coverage condition"
The suggested flag to "allow undecidable instances" is throwing me
off, since it seems very unambiguously decidable to me.
Regards,
Philip
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
