On 9 June 2015 at 14:48, Matt Oliveri <[email protected]> wrote:
>
> It's true that dependent types and refinement types can look very
> similar, but there's a real difference. I can't explain it simply,
> just point out that it causes problems in most forms of dependent type
> theory, but not in Nuprl. Nuprl has an unusual set of deduction rules
> that allow you to use well-typed terms (proofs) to establish that some
> other term (program) has a certain type. It has some other odd stuff
> too. The subtlety is why you truly lose expressiveness without this
> (as a programming language; logics can do without it), and why there's
> no good workaround.
>
Yes, I think Nuprl is extensional, but this has other problems. HoTT tries
to
dance the line between intensional and extensional.
I don't plan on using dependent types, but instead on lifting values, which
I don't think
has these problems.
> 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
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 ...
> 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.
> 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.
My problem is I started making point (2), and used the notation I am
working with, and you focus on (1) not (2).
This whole discussion started with point (2), so I am just trying to steer
it back on topic.
> > This can apply to refinement types as they are. Basically I am
> > saying that functions define the constraints, which you propagate back to
> > the definition. Here's an example:
> >
> > showDie (x : (Integer a, LessThan 6 a) => a) = putStrLn x
> > id x =x
> > main = showDie (id 3))
> >
> > The constraint is propagated through id, to the literal 3, where we can
> test
> > if 3 satisfies the constraint (its an integer less than 6). If you cannot
> > get used to writing the constraints like type classes I could write them
> > like this:
> >
> > showDie :: {x : Integer | x < 6} -> IO ()
> >
> > To argue for the type-class representation, we are effectively defining a
> > subtype, You should read the 'LessThan' constraint as "the value of a is
> > less than 6".
> >
> > I could also write:
> >
> > data Die x = Die {a : Int | a < 6}
> > showDie (Die x) = putStrLn x
> > main = showDie (id (Die 3))
> >
> > Now, I would like that the first version of showDie be possible, I am not
> > (yet) banning the second with a datatype for Die :-)
>
> 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.
Keean.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
