Re: [Haskell-cafe] Ur tutorial, and a challenge
On Wed, Jul 27, 2011 at 8:30 AM, Christopher Done wrote: > On 27 July 2011 13:58, Adam Chlipala wrote: >> Does this static type system support metaprogramming strong enough to >> implement my challenge problem with the level of static guarantee for all >> specialization parameters that I ask for? > > Again I don't really know what you're talking about so I'll drop it. Here's a question that I suspect may be relevant: Can you generate code with TH that isn't well-typed? If your first thought is something like "of course, how would you type check the code before generating it?", I would ask how that differs from "of course programs can crash, how can you check all inputs before reading them at run time?". Bonus question for any OCaml folks: What's the difference between using Camlp4 and using MetaOCaml? - C. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Ur tutorial, and a challenge
On 27 July 2011 13:58, Adam Chlipala wrote: > Maybe, but I don't think you've outlined any solutions that meet my > criteria. The key property is what I've highlighted in my self-quote above: > the challenge is to type-check _the_code_generator_, not just the individual > programs it generates. I want a static theorem that every program coming > out of the code generator will play by the rules. No, I didn't outline any solutions for that criteria. I'm not competent to answer that. >> Yesod employs static typing for templates. > > Does this static type system support metaprogramming strong enough to > implement my challenge problem with the level of static guarantee for all > specialization parameters that I ask for? Again I don't really know what you're talking about so I'll drop it. Agda is still on my list of things to learn. As is Ur. But that order seems appropriate. Ciao! ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Ur tutorial, and a challenge
Christopher Done wrote: On 19 July 2011 17:22, Adam Chlipala wrote: http://www.impredicative.com/ur/demo/crud1.html [...] This is not done by type-checking individual invocations of the admin-interface component. Rather, the component is checked at a static type which guarantees correct operation for _any_specialization_parameters_. So, the challenge is, can this functionality be implemented in Haskell (GHC extensions fair game, any web framework allowed)? Is TemplateHaskell fair game? Sure. Because if so these problems are not hard. Maybe, but I don't think you've outlined any solutions that meet my criteria. The key property is what I've highlighted in my self-quote above: the challenge is to type-check _the_code_generator_, not just the individual programs it generates. I want a static theorem that every program coming out of the code generator will play by the rules. Even rules that are trivial to check for individual programs (e.g., no code injection attacks because you follow a simple AST discipline) become quite non-trivial when you are reasoning about the behavior of a code generator. Also, this "simple" property gets more interesting when you also want to enforce statically, e.g., that all SQL queries are type-correct w.r.t. the database. Yesod employs static typing for templates. Does this static type system support metaprogramming strong enough to implement my challenge problem with the level of static guarantee for all specialization parameters that I ask for? HaskellDB achieves injectionless static type checking even without TemplateHaskell Right. Easy to do for individual programs, harder to do for a code generator. and templatepg has type safe SQL queries based on parsing the SQL itself and inspecting the types involved by asking the PostgreSQL server directly at compile time. Ur/Web does this, too, as a kind of belt-and-suspenders measure. This alone provides no support for static checking of metaprograms. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Ur tutorial, and a challenge
Excerpts from Christopher Done's message of Wed Jul 27 12:26:08 +0200 2011: > Is TemplateHaskell fair game? Because if so these problems are not > hard. Yesod employs static typing for templates. HaskellDB achieves > injectionless static type checking even without TemplateHaskell, and > templatepg has type safe SQL queries based on parsing the SQL itself > and inspecting the types involved by asking the PostgreSQL server > directly at compile time. Which doesn't work because the result of querying is not accurate enough (or has not been in the past?).. Eg see here -> Only DB2 seems to return usable results. http://www.haskell.org/haskellwiki/MetaHDBC The main problem is: Does a field return a nullable value (thus Maybe?) However if that changed I want to know about it :) If you know databases inside out than you also know that its sometimes faster to run a sophisticated custom query than doing all the work in Haskell (after sending data over network). Don't think HaskellDB supports all of those features. I imagine that its easier to extend urweb in this regard. However there are a lot new SQL based Haskell libraries I don't know yet. The difference is that Haskell's type system is bad at creating temporary types unless you go the HList route? http://hackage.haskell.org/package/records Does this library address this? While Haskell's type system is known to be touring complete this doesn't mean that such code is easy to maintain. I'm no longer up to date so all I said may be partially wrong :( Marc Weber ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Ur tutorial, and a challenge
On 19 July 2011 17:22, Adam Chlipala wrote: > http://www.impredicative.com/ur/demo/crud1.html > The example involves a library component encapsulating functionality like > that of Ruby on Rails's scaffolding: automatic generation of a standard > web-based "admin interface" to an SQL database table. The Ur/Web version > uses static typing to guarantee that any applications generated by this > component are free of injection attacks and other generic problems. The > guarantees apply both to app communication with server-side pieces (e.g., > static type-checking of SQL) and client-side pieces (e.g., static > type-checking of HTML). This is not done by type-checking individual > invocations of the admin-interface component. Rather, the component is > checked at a static type which guarantees correct operation for > _any_specialization_parameters_. > > So, the challenge is, can this functionality be implemented in Haskell (GHC > extensions fair game, any web framework allowed)? Is TemplateHaskell fair game? Because if so these problems are not hard. Yesod employs static typing for templates. HaskellDB achieves injectionless static type checking even without TemplateHaskell, and templatepg has type safe SQL queries based on parsing the SQL itself and inspecting the types involved by asking the PostgreSQL server directly at compile time. This doesn't protect you from runtime changes to the DB schema of course. I think there's a lot of interesting work to be done based on inspecting the data base schema by querying the database server and analyzing queries at compile time. Ferry, anyone? Statically avoiding SQL and HTML injection/type problems are trivial problems that have been solved since forever ago, I don't think those are Ur's best secret weapon (dependent types goes without saying). Of Ur I particularly like that you can write Ur that will be compiled to JS. That is something that is hard to do in Haskell right now (ghcjs is a great base, but it's alpha). I don't anyone will spend time to answer the crud challenge. > If so, how pretty is it? > :) Anything's gonna be prettier than what you've presented there. ;-) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Ur tutorial, and a challenge
Last week, I posted a message to this list looking for people interested in joining projects using my domain-specific language Ur/Web. Some responses rightly chastised me for the lack of documentation on the core Ur language's novel type system features. I'm sure many Haskellers have had the experience of quickly grokking the interfaces of new libraries by reading their type signatures, and I think the same is true for Ur. So, to provide that initial bump of background that should help folks get started, I've begun an Ur tutorial: http://www.impredicative.com/ur/tutorial/ The chapters that are already there are intended to be sufficient to help any experienced Haskell programmer get started quickly with Ur/Web. In particular the second chapter on type-level programming may be of interest as a mind expander, even for folks who don't want to use Ur/Web. I'd love feedback about weaknesses in the tutorial! I also want to attach a challenge to this tutorial, as an expansion to an answer I gave earlier about why Ur/Web needs a new programming language and can't just be implemented as a Haskell library. Consider this online Ur/Web demo: http://www.impredicative.com/ur/demo/crud1.html The example involves a library component encapsulating functionality like that of Ruby on Rails's scaffolding: automatic generation of a standard web-based "admin interface" to an SQL database table. The Ur/Web version uses static typing to guarantee that any applications generated by this component are free of injection attacks and other generic problems. The guarantees apply both to app communication with server-side pieces (e.g., static type-checking of SQL) and client-side pieces (e.g., static type-checking of HTML). This is not done by type-checking individual invocations of the admin-interface component. Rather, the component is checked at a static type which guarantees correct operation for _any_specialization_parameters_. So, the challenge is, can this functionality be implemented in Haskell (GHC extensions fair game, any web framework allowed)? If so, how pretty is it? :) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
