Ur/web: pure functional, statically typed web programming(impredicative.com)

104 pointsby dpkgreconfigurevor 12 Jahren45 comments

Ur/web: pure functional, statically typed web programming

http://impredicative.com/ur

12 comments

bhauervor 12 Jahren

A brief note on performance: Ur/web has been in recent rounds of our project and has performed exceptionally well. For instance, achieving 112,807 Fortunes responses per second on our Peak Hosting hardware:

http://www.techempower.com/benchmarks/#section=data-r9&hw=pe...

And the code for the same:

https://github.com/TechEmpower/FrameworkBenchmarks/blob/mast...

ajbvor 12 Jahren

This is kind of radical, I wonder how well it works in practice:

"The Ur/Web compiler is unconventional in that it relies on a kind of heuristic compilation. Not all valid programs will compile successfully. Informally, programs fail to compile when they are “too higher order.” Compiler phases do their best to eliminate diﬀerent kinds of higher order-ness, but some programs just won’t compile. This is a trade-oﬀ for producing very eﬃcient executables. Compiled Ur/Web programs use native C representations and require no garbage collection."

jbapplevor 12 Jahren

C++ has a similar (though more carefully specified) limit on template instantiation depth.

I would be surprised if this were not true in practice for all compiled languages - some programs will be too large to compile given the memory constraints of the machine the compiler is running on.

ajbvor 12 Jahren

That wouldn't be radical, I agree. But unless I'm missing something the limitation is much less easy to predict: it's which programs can the compiler analyse the runtime memory usage of. That's why I'm curious about what it means in practice.

Dewievor 12 Jahren

> I would be surprised if this were not true in practice for all compiled languages - some programs will be too large to compile given the memory constraints of the machine the compiler is running on.

Clearly this is different to a compiler which intentionally rejects programs that can't be efficiently implemented/compiled.

jbapplevor 12 Jahren

> Clearly this is different to a compiler which intentionally rejects programs that can't be efficiently implemented/compiled.

I agree.

I wonder what happens when the heuristic fails in the Ur/web compiler. When my C++ compiler runs over its template instantiation depth, I get a nice error message telling me what happened and how to increase the depth.

mazsavor 12 Jahren

"I know of only one "provably correct" web-application language: UR. A Ur-program that "goes through the compiler" is guaranteed not to:

Suffer from any kinds of code-injection attacks

Return invalid HTML

Contain dead intra-application links

Have mismatches between HTML forms and the fields expected by their handlers

Include client-side code that makes incorrect assumptions about the "AJAX"-style services that the remote web server provides

Attempt invalid SQL queries

Use improper marshaling or unmarshaling in communication with SQL databases or between browsers and web servers"

https://stackoverflow.com/questions/4065001/are-there-any-pr...

cgagvor 12 Jahren

I think yesod (http://www.yesodweb.com/) manages to achieve a decent amount of this stuff in Haskell.

cabalamatvor 12 Jahren

This language was inspired by Haskell, however it is unfortunately more verbose. Consider:

    fun mp [a] [b] (f : a -> b) : list a -> list b =
        let
            fun loop (ls : list a) =
                case ls of
                    [] => []
                  | x :: ls' => f x :: loop ls'
        in
            loop
        end

Which in Haskell would be:

    map :: (a->b) -> [a] -> [b]
    map _ [] = []
    map f x:xs = (f x):(map f xs)

Or this notation for lists:

    2 :: 3 :: 4 :: []

Cf Haskell:

    [2,3,4]

ajbvor 12 Jahren

It looks more like ML than haskell. But the explicit return of a function and explicit case aren't necessary in ML either, so I'm not sure why they are used here. A quick scan of the reference manual finds mention of currying, but I don't see anything about pattern matching without case statements, so maybe the language doesn't have that.

freyrs3vor 12 Jahren

The map example with toplevel pattern matching is really just sugar for the expanded case statements which isn't that far from the Ur equivalent.

  map :: forall a b. (a -> b) -> [a] -> [b]
  map =
    \ (@ a) (@ b) (ds :: a -> b) (ds1 :: [a]) ->
      case ds1 of _ {
        [] -> [];
        : x xs ->
          (ds,x,xs) : ((ds,x) ds x) ((ds,xs) map ds xs)
      }

cabalamatvor 12 Jahren

> The map example with toplevel pattern matching is really just sugar for the expanded case statements which isn't that far from the Ur equivalent

And both the Ur and the Haskell are really just sugar for a load of machine code. The reason I prefer the more compact Haskell version is that it allows me to express what I mean more precisely; other things being equal, a more compact notation will be higher-level and thus closer to how humans think.

gizmo686vor 12 Jahren

Note that the Haskell list notation is just syntactic sugar. [2,3,4] gets translated directly into

    2:3:4:[]

cabalamatvor 12 Jahren

Sure, it's syntactic sugar, but there's no "just" about it -- being able to express ideas more concisely helps readability.

sixbrxvor 12 Jahren

I think List plays a much more integral role in Haskell than it would in a strict language like this. In Haskell, list is irreplaceable because it can correspond to a value and a thunk for the rest of a result stream, so it's a very special data structure because of the relationship to the language's laziness.

In a strict language though, the list is just a list - nothing special, and users may want to replace it with library variants with different performance tradeoffs (this even happens in Haskell of course for some problem areas). Since this is the case, a uniform treatment may be preferred, where the type name is just like any other type name, construction is just as any other type's construction, and the type is in fact just supplied by a library not the compiler. I don't know if this was the developers' thinking (I'm not involved), but uniformity has its advantages.

Also, I don't think it's really clear that [] is easier to read, especially when it's surrounded by other syntax like parens and braces - it doesn't stand out much, which can be good or bad depending on personal preferrences and the surroundings. Rust recently moved from [] -> Vec for vectors and I think it's easier to read that way, personally.

sixbrxvor 12 Jahren

It's because the more advanced features that it has over Haskell in type-level computation make its type inference undecidable. http://impredicative.com/ur/tutorial/tlc.html

dilapvor 12 Jahren

As used by bazqux.com, an RSS reader; I've been trying it out for the last couple weeks, and so far the core functionality has been rock solid, unlike any of the multiplicity of other readers I've tried since Google Reader died. (Unfortunately, the site's design leaves a lot to be desired, including any mobile-friendly version at all...)

jdfvor 12 Jahren

I've been using BazQux since the Google Reader close and have been pretty happy with it. I don't think I've noticed a single issue with BazQux so far.

The web interface is actually quite snappy, in contrast to a lot of the overly-designed alternatives I tried out. That said, I generally interface with FeeddlerPro on my phone/tablet rather than directly hitting bazqux.com.

Ycrosvor 12 Jahren

The first thing that grabbed me about bazqux was just how fast and responsive it felt to use. The second thing was that it was the closest replacement to Google Reader I had come across. I'm still using it.

michaelmiorvor 12 Jahren

To be fair, I'm guessing that BazQux is not getting the same amount of traffic as many of the other alternatives. FWIW, I've been using The Old Reader[1] quite successfully since Google Reader went away.

[1] http://theoldreader.com/

Qerubvor 12 Jahren

See also: The Opa Framework at http://opalang.org/.

(Comparison on http://www.impredicative.com/ur/opa/.)

jkarnivor 12 Jahren

What exactly are row types? I believe Ermine also features them, but searching doesn't yield very informative results.

tikhonjvor 12 Jahren

Row types refer to row polymorphism. It's a kind of polymorphism that lets you write code that's generic over different records with different fields without using subtyping.

Lets say you want to write a function that takes anything with a .length field:

    maxByLen a b = if a.length > b.length then a else b

How would you come up with the types for this? In a Java-like system of nominative sub-typing, you would make an interface Length and require types to declare it explicitly. However, this is messy, completely unnecessary and messes up type inference, so it's not a good idea.

You could also use structural sub-typing. You could declare the function to have a type like

    byLength : { length : Int } -> { length : Int } -> { length : Int }

where any record with a field length of type Int has the type { length : Int }. In other words, the type { length : Int, name : String } is a subtype of { length : Int } without needing to declare an interface explicitly. This is a definite improvement over the nominative Java case.

There are a couple of problems with this, however. A major one is that it "throws away" type information. In particular, all you know about either argument is that they have length fields. They might otherwise be of different types, with all their other fields completely different. You could compare a Foo and a Bar, as long as they both have lengths. Also, if you return something of the argument type, all you will know about it after that is that it has a length field; you've lost its actual type statically. To cast back up would require a potentially failing runtime check.

Consider that if we have two type Foo { length : Int, name : String} and Bar { length : Int, height : Int }, we can pass one of each into the function. Then which one it returns depends on runtime data: it might be a Foo and it might be a Bar. This means we cannot know the specific return type; all we know now is that it has to have a length field.

This is very different from normal parametric polymorphism which has type variables. While you don't know anything about the variable inside the function, it doesn't throw out type information when its used. For example, imagine this code instead:

    maxBy : (a -> Int) -> a -> a -> a
    maxBy pred a b = if pred a > pred b then a else b

This one can be used the same way by passing in a length function. However, since it doesn't use subtyping, both arguments have to have the same type! This means we can't use it to compare a foo and a bar. But when we do use it on Foos, for example, we know we will get a Foo out because that's what the a variable will be unified to:

    (a -> Int) -> a -> a -> a
    (Foo -> Int) -> Foo -> Foo -> Foo

When we use the function on a Foo, a gets instantiated to Foo giving us the second type.

Row types are just a way to bring this second style of polymorphism to records with different fields. Basically, it allows you to put a type variable representing the "rest" of the record:

    maxByLen : { length : Int | r } -> { length : Int | r } -> { length : Int | r }

Now, when we use this on a Foo, r gets instantiated to { name : String }; when we use it on a Bar, it gets instantiated to { height : Int }. This means we can't mix Foos and Bars and we don't lose type inference.

It also lets us do some other nice things. For example, we could add a field, polymorphically:

    annotate : { length : Int | r } -> { length : Int, lenStr : String | r }

It's also nice to note that we don't lose anything: we can get something very similar to the old behavior by throwing information away explicitly:

    maxBy : { length : Int | a} -> { length : Int | b } -> { length : Int }
    maxBy a b = if a.length > b.length then { length = a.length }
                                       else { length = b.length }

We can get almost exactly the sub-typing behavior by using existential types:

    maxBy : (exists a. { length | a }) -> (exists b. { length | b }) -> 
               (exists c. { length | c })
    maxBy a b = if a.length > b.length then a else b

I'm not sure why we would want this though! (I also don't know if any languages support this sort of syntax exactly, so you might have to jump through some additional hoops to simulate "exists".)

As a final note, I haven't used row polymorphism or existential types very much, so there might be some mistakes above.

It's also worth noting that Ermine has a slightly more general form of row polymorphism, but I'm not sure what the specific differences are.

thinkpad20vor 12 Jahren

Very interesting writeup! Thanks. This now gives me more ideas to use in the language I'm working on.

I independently had what seems to be a similar idea, which is sort of like "anonymous type classes." For example, Vectors, Lists, Strings, Maps, Sets, etc all have something like a "size" function. So say there exist functions like

    size : Vector a -> Int
    size : String -> Int
    size : List a -> Int
    ...

And say we wanted to make a function like:

    show_size a = show a + " has a size of " + show (size a)

To write this in Haskell, you'd have to create a `Size` type class:

    class Size a where size :: a -> Int

And then write instances for all of them. And you'd have to do the same for `show`. But that's almost as tedious as the Java example. Now a Haskell type class is essentially a set of named function signatures, so instead, you can create a type class "on the fly":

    show_size : a of {size: a -> Int, show: a -> String} -> String

The cool thing here is that you keep the type information, in a similar way to what you were describing:

    foo : a of {f: a -> b -> Int} -> b of {g: b -> Int -> b} -> b
    foo a b = g b (f a b + 10)

So here we know that as long as there exist appropriate `f`s and `g`s, then we can pass any `a` and any `b` in and get a `b` back.

tompvor 12 Jahren

I reckon this is based on Daan Leijen's awesome (and very readable) paper "Extensible records with scoped labels" [1]. It's also quite simple to implement, I've done it here [2] (in OCaml).

[1] http://research.microsoft.com/apps/pubs/default.aspx?id=6540... [2] https://github.com/tomprimozic/type-systems/tree/master/exte...

skybrianvor 12 Jahren

It looks like Elm has this?

http://elm-lang.org/learn/Records.elm

CountHackulusvor 12 Jahren

That was an excellent writeup. Just want to say thank you. Somewhat hilariously, this is somewhat similar to some COBOL functionality I've seen.

mthqvor 12 Jahren

Row types are a way to encode type information of OOP object in a hindley milner type system. It allows you to type check the kind of ducked objects that are often featured in dynamic OOP languages like ruby and javascript. So you may specify a function on a object containing specific fields or methods without specifying a concrete type:

  f :: {left: Number, right: Number} -> Number
  f object = object.a + object.b

All type checked of course.

See here for more info: https://www.cs.cmu.edu/~neelk/rows.pdf

roryokanevor 12 Jahren

I assume you meant to write `object.left + object.right` instead of `a` and `b`, to match the type signature.

julesvor 12 Jahren

Row types are an alternative to subtyping for record/object types. With subtyping you say that if you have a record Foo and you leave out some fields to get a record Bar then Foo is a subtype of Bar. For example the type {a:int, b:string} is a subtype of {a:int}. This means that if you have a function f : {a:int} -> ResultType, then you can pass a value of type {a:int, b:string} to it, since it has all the required fields. A problem with subtyping for records/objects is that it doesn't work very well with type inference.

With row types you use parametric polymorphism to make the extra fields explicit. You have types of the form {a:int, ...B} where B indicates that the value may have additional fields. In this system you give f the type forall B. {a:int, ...B} -> ResultType.

Row types are more powerful than subtyping in some ways but less powerful in other ways. For example with subtyping you can put two records {a:3, b:"hello"} and {a:5} in the same list. With row types you can't do that (you'd need existential types to do that). It turns out that these restrictions make type inference for row types decidable.

kahoonvor 12 Jahren

Just a suggestion: a landing page should immediately show some captivating examples telling me why I should be interested.

thinkpad20vor 12 Jahren

Agreed. Code samples are one of the most effective ways to communicate an idea of how ones library/language/whatever works. Also, a layout that doesn't make it look like the site was written in 1996...

nlyvor 12 Jahren

Linked from the "Who's using it" page:

https://github.com/bazqux/bazqux-urweb

[deleted]vor 12 Jahren

kilowattvor 12 Jahren

Using React every day has me sold on functional reactive programming for UI. But there's definitely some friction at the boundary between the nicely declarative React tree and the rest of the world with all its mutable state.

I'd love to experiment with with React and Elm (or maybe Ur/web?) together.

andreypoppvor 12 Jahren

You could also be interested in PureScript[1] then; and its React bindings[2]. It is a statically typed language which compiles to JS. It has row polymorphism and effects (yay!).

[1]: http://purescript.org [2]: https://github.com/purescript-contrib/purescript-react

cgagvor 12 Jahren

This is the stack I'm planning on attemtping to use for my next project. The purescript-react docs could use some work, and I think the best example is the one in the pull request "Another example", but it seems like purescript + react is a really nice combo.

teamonkeyvor 12 Jahren

Given that Elm is a FRP language, what additional benefit does React grant you?

steschvor 12 Jahren

The demo code on http://impredicative.com/ur/demo/ mixes HTML with ur. Is this some kind of functional PHP?

No real templates?

klibertpvor 12 Jahren

The difference is that the HTML in Ur/Web is not just a string like in PHP. Ur provides a special syntax for building XML trees and so if you include the code like "<b>something<b" in Ur/Web it just won't compile. You can't ever output malformed HTML in Ur.

This also allows for type checking of HTML - for example you can be sure that you won't have unescaped output in your HTML because the type system makes it impossible (won't compile) to use unescaped string in place of escaped one.

So in short, what you saw already is a template engine (also look at React (and maybe Opa?), which also has a special syntax for building XML/HTML), and it's already insanely powerful.

octagonalvor 12 Jahren

People would be more easily convinced of Ur/web's usefulness if impredicative.com/ur didn't look straight out of 1995.

Dewievor 12 Jahren

What more do you want from a language homepage?

mikegioiavor 12 Jahren

It (unfortunately or not) has a lot to do with whether someone spends more than 20 seconds investigating it.

desireco42vor 12 Jahren

Am I the only one who notices that for web framework, website is horrendous. The problem with these experiments, in my humble view is that they are disconnected from medium in which it is suppose to work.

pessimizervor 12 Jahren

The overlap between web programming and web design is similar to the overlap between oil painting and bowls of fruit.

desireco42vor 12 Jahren

This is not about web design :) this is about not knowing the medium you are supposedly working on. It's like you are developing mobile apps, but don't care about usability.