On Tue, Jun 9, 2015 at 11:10 AM, Keean Schupke <[email protected]> wrote: > On 9 June 2015 at 14:48, Matt Oliveri <[email protected]> wrote: >> As for how _you're_ planning to do value lifting, well I'm still >> interested in seeing some code that does it. And the way you >> interpreted range types didn't sound like lifting either, and I don't >> think it could even compete with dependent types, let alone refinement >> types. > > Well there is code in the HList paper that does it, but its really simple: > > {-# LANGUAGE RankNTypes #-} > > data Z = Z deriving Show > data S x = S x deriving Show > > lift' :: Show a => a -> Int -> (forall a. Show a => a -> IO ()) -> IO () > lift' a x f | x == 0 = f a > lift' a x f | x /= 0 = lift' (S a) (x - 1) f > > lift = lift' Z > > cont :: Show a => a -> IO () > cont x = putStrLn $ show x > > main = lift 3 cont
This is not the kind of thing I was expecting. lift "computes" the right type internally, but it seems you never get to refer to it, except as an argument in a continuation. So I guess you're planning to translate everything to CPS? It seems hard/impossible to relate two lifted values this way. I should probably say now that if it turns out you use a whole-program transformation to express what I want, I will not accept your approach as a solution. > Note, in Haskell the requirement to give a complete type signature for the > polymorphic-recursion > means it does not infer the constraints. A future expansion for partial type > signatures will allow something like: > > lift' :: _ => a -> Int -> (forall a. _ => a -> IO ()) -> IO () > > I won't be requiring this though, literals will lift directly to types > automatically, so you just need: > > let x = 3 in ... Wait, let me get your story straight. You're saying you can translate automatic lifting to CPS "lift" above? If so, you need to convince me. If not, why the heck are we talking about Haskell, since you are apparently using a different type system without letting me know? >> So no, I don't think our two interpretations of range types are the same >> at all. > > I think they are, but perhaps I am not explaining it well. Really the only > difference is syntax. Well, depending on how "the same" you think they are, that's either very hard to believe, or a useless fact of no practical importance. Assuming you're not arguing a useless fact, we will just have to continue to discuss your system, so I can get to the bottom of any possible differences. >> > 2. I also pointed out that I don't think annotating types with >> > constraints >> > is the right way to go, for reasons of code reuse, and application >> > architecture. >> >> I don't think I confused these two things you're saying. I just >> objected to you talking about number 2 in response to what I was >> saying about number 1. It's very hard to reach any conclusions in >> discussions with you. You tend to just move from one point to another >> without explanation. Will we ever find out who was understanding >> Shap's range types better? Only if Shap tells us. And if I was closer, >> will you learn anything from your misunderstanding? Or will you be too >> busy disagreeing with me on something else? Who knows? > > I cannot prove the constraints I am proposing are the same as refinement > types, although I am convinced they are. > If you give me any program using > refinement types I should be able to > translate it into my notation with only a syntactic change. Let's start simple: (* Recall that nat has constructors O (zero) and S (successor) *) Inductive Even : nat->Prop := ez : Even O | ess n : Even n->Even (S (S n)). Definition even10 : Even 10 := ess 8 (ess 6 (ess 4 (ess 2 (ess 0 ez)))). > My problem is I started making point (2), and used the notation I am working > with, and you focus on (1) not (2). Well (1) and (2) were different subthreads. I was focusing on (1) in the subthread replying to Shap regarding range types. > This whole discussion started with point (2), so I am just trying to steer > it back on topic. Yes, but there was a separate subthread for that, which I'm guessing you will never reply to, now that you've moved both topics onto this subthread. :\ >> Yet more partial examples get you only so far with me. I need to see a >> complete example, including the polymorphic recursion you claim to be >> able to define lifting with. In addition to just seeing what the heck >> things like LessThan above are, I need to see how those type >> classes--which sound like they should've been predicates--fit with the >> type classes that sound like they should've been types. > > Those are complete examples, but they are in a Haskell like language that > has > the features I am discussing in point (1). You only need polymorphic > recursion in Haskell > because it does not support automatic lifting of constants. I see. This partially answers one of my questions above, but please do answer above in your reply, to confirm. But still, I did not see a definition of LessThan, for example. But I'm not asking for it yet. I just want one complete example in your extended system, for starters. Pick whichever's easiest. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
