Hacker News Reader

Comment by tinco | Hacker News Reader

It's interesting, but is it powerful enough? There's a great talk by Zed Shaw about implementing authorization code. I think the same issue holds here.

A language might work for simple and more complex type constraints, but at some point the constraints might become so weird that you really need a full blown turing complete language to define them.

And that point might be sooner than you'd like. Why not instead of using expressions in this constrained language, use something like Haskell?

It's got the super powerful typesystem, and you're certain that it will be able to express any constraint you throw at it.

That said, this language does look nice, and I haven't really tried to find out if there's any obviously important constraints you wouldn't be able to build in it.

View on HN

> Why not instead of using expressions in this constrained language, use something like Haskell?

Haskell types can't depend on values so there are limitations. If you go that way, you might as well go whole hog and use a dependently typed language (e.g. Idris)

This one?

http://vimeo.com/2723800

Yes that's the one :)

(a) As others have said, Haskell's type system is certainly now powerful enough to express any constraint you throw at it.

(b) Almost directly related to that, the less powerful your constraint language the more analyzable it is. I don't necessarily know that Q has these properties, but by constraining how complex the restrictions it encodes are it becomes more amenable to analysis. At first blush, it looks like you'd probably be able to throw a SMT solver at it quite easily.

> is certainly now powerful enough

Small typo there.

Ha, small vital one—obviously meant 'not'. Thanks!

> It's got the super powerful typesystem, and you're certain that it will be able to express any constraint you throw at it.

You can go pretty far with, eg, Java, if you're ready to pay the cost in verbosity, by making types for everything and having read-only objects. Haskell is not dependently typed, you can't use the type system to make sure a value is in a given range. You could use phantom types to make sure your type has been validated before, but this kind of control is not really first-class.

You might want to embed this inside a larger language. That wouldn't necessarily preclude using a Turing Complete language, but you wouldn't want it to be a complicated one.

Reply on news.ycombinator.com