Re: [Haskell-cafe] type-level integers using type families
Peter Gavin wrote: Roberto Zunino wrote: Maybe he wants, given cond :: Cond x y z = x - y - z tt :: True true_exp :: a false_exp :: untypable that cond tt true_exp false_exp :: a That is the type of false_exp is lazily inferred, so that type errors do not make inference fail if they show up in an unneeded place. Yes, that's exactly what I want, but for type families (not MPTC). I think it could be done if the type arguments were matched one at a time, across all visible instances. What do you think of the following idea? Using naive type level natural numbers, data Zero newtype Succ a = Succ a Booleans, data True data False comparison, type family (::) x y type instance (Zero :: Succ a) = True type instance (Zero :: Zero ) = False type instance (Succ a :: Zero ) = False type instance (Succ a :: Succ b) = a :: b difference, type family Minus x y type instance Minus aZero = a type instance Minus (Succ a) (Succ b) = Minus a b and a higher order type level conditional, type family Cond2 x :: (* - * - *) - (* - * - *) - * - * - * type First2 (x :: * - * - *) (y :: * - * - *) = x type Second2 (x :: * - * - *) (y :: * - * - *) = y type instance Cond2 True = First2 type instance Cond2 False = Second2 we can define division as follows: type family Div x y type DivZero x y = Zero type DivStep x y = Succ (Div (Minus0 x y) y) type instance Div x y = Cond2 (x :: y) DivZero DivStep x y It's not exactly what you asked for, but I believe it gets the effect that you wanted. Enjoy, Bertram ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type-level integers using type families
Manuel M T Chakravarty wrote: Peter Gavin: will work if the non-taken branch can't be unified with anything. Is this planned? Is it even feasible? I don't think i entirely understand the question. Maybe he wants, given cond :: Cond x y z = x - y - z tt :: True true_exp :: a false_exp :: untypable that cond tt true_exp false_exp :: a That is the type of false_exp is lazily inferred, so that type errors do not make inference fail if they show up in an unneeded place. If we had subtyping, typing that as Top would suffice, I believe. Zun. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type-level integers using type families
Peter Gavin wrote: Has anyone else tried implementing type-level integers using type families? I tried using a couple of other type level arithmetic libraries (including type-level on Hackage) and they felt a bit clumsy to use. I started looking at type families and realized I could pretty much build an entire Scheme-like language based on them. In short, I've got addition, subtraction, multiplication working after just a days worth of hacking. I'm going to post the darcs archive sometime, sooner if anyone's interested. I really like the type-families based approach to this, it's a lot easier to understand, and you can think about things functionally instead of relationally. (Switching back and forth between Prolog-ish thinking and Haskell gets old quick.) Plus you can do type arithmetic directly in place, instead of using type classes everywhere. nice, it's been tried before, etc. etc.. And of course it doesn't work with a released version of GHC, so maybe it's hoping too much that it would be on Hackage. What I was going to say was, see if there is one on hackage, otherwise there should be one there to be polished. But I guess searching haskell-cafe is your man :-) (your way to try to find any. Or the Haskell blogosphere too.) One thing that I'd like to be able to do is lazy unification on type instances, so that things like ... will work if the non-taken branch can't be unified with anything. Is this planned? Is it even feasible? I'm pretty sure it would be possible to implement a Lambda like this, but I'm not seeing it yet. Any ideas? Yeah -- that would be neat but generally tends to lead to undecidability (unless you're really careful making it a lot(?) less useful). That is, potential nontermination in the type inferencer/checker, not just in runtime. Then you'll want it to be well-defined when something is type-level-lazy, so you can reliably write your type-level algorithms. And *that* is bound to be rather difficult to define and to implement and maintain. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type-level integers using type families
Peter Gavin: Has anyone else tried implementing type-level integers using type families? I tried using a couple of other type level arithmetic libraries (including type-level on Hackage) and they felt a bit clumsy to use. I started looking at type families and realized I could pretty much build an entire Scheme-like language based on them. In short, I've got addition, subtraction, multiplication working after just a days worth of hacking. I'm going to post the darcs archive sometime, sooner if anyone's interested. I really like the type-families based approach to this, it's a lot easier to understand, and you can think about things functionally instead of relationally. (Switching back and forth between Prolog- ish thinking and Haskell gets old quick.) Plus you can do type arithmetic directly in place, instead of using type classes everywhere. I am glad to hear that type families work for you. One thing that I'd like to be able to do is lazy unification on type instances, so that things like data True data False type family Cond x y z type instance Cond True y z = y type instance Cond False y z = z will work if the non-taken branch can't be unified with anything. Is this planned? Is it even feasible? I don't think i entirely understand the question. Do you mean that from an equality like Cond b Int Bool ~ Int you want the type checker to infer that (b ~ True)? This is generally not correct reasoning as type families are open; ie, subsequent modules might add data Bogus type instance Bogus y z = Int and now there are two solutions to (Cond b Int Bool ~ Int). Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] type-level integers using type families
Has anyone else tried implementing type-level integers using type families? I tried using a couple of other type level arithmetic libraries (including type-level on Hackage) and they felt a bit clumsy to use. I started looking at type families and realized I could pretty much build an entire Scheme-like language based on them. In short, I've got addition, subtraction, multiplication working after just a days worth of hacking. I'm going to post the darcs archive sometime, sooner if anyone's interested. I really like the type-families based approach to this, it's a lot easier to understand, and you can think about things functionally instead of relationally. (Switching back and forth between Prolog-ish thinking and Haskell gets old quick.) Plus you can do type arithmetic directly in place, instead of using type classes everywhere. One thing that I'd like to be able to do is lazy unification on type instances, so that things like data True data False type family Cond x y z type instance Cond True y z = y type instance Cond False y z = z will work if the non-taken branch can't be unified with anything. Is this planned? Is it even feasible? I'm pretty sure it would be possible to implement a Lambda like this, but I'm not seeing it yet. Any ideas? Pete ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
