News for hackers. Stuff that matters.
Re:Learn You an Agda by pseudonom- on Tuesday December 02, 2014 @06:26PM (#8690815)
It's not exactly what you're asking for but Ur/Web puts an expressive type system to some slightly unusual ends: http://www.impredicative.com/ur/.
Re:Learn You an Agda by kyllo on Tuesday December 02, 2014 @08:29PM (#8691322)
Whoa, this is pretty horrifying: app code, queries and markup all mixed together, like typed-checked PHP. I know this is just a demo but "separation of concerns" does not appear to have been a concern.

    fun list () =
            rows <- queryX (SELECT * FROM tab AS T)
                           (fn (fs : {T : $([Id = int] ++ map fst M.cols)}) => <xml>
                             <tr>
                               <td>{[fs.T.Id]}</td>
                               {@mapX2 [fst] [colMeta] [tr]
                                 (fn [nm :: Name] [t ::_] [rest ::_] [[nm] ~ rest] v col => <xml>
                                   <td>{col.Show v}</td>
                                 </xml>)
                                 M.fl (fs.T -- #Id) M.cols}
                               <td>
                                 <a link={upd fs.T.Id}>[Update]</a>
                                 <a link={confirm fs.T.Id}>[Delete]</a>
                               </td>
                             </tr>
                           </xml>);
Re:Learn You an Agda by foobarbaz1234 on Wednesday December 03, 2014 @05:29AM (#8692909)
Keep also in mind, that it is ultra-fast (http://www.techempower.com/benchmarks/#section=data-r9&hw=pe...).
Re:Learn You an Agda by pron on Tuesday December 02, 2014 @06:50PM (#8690930)
Oh, nice! Indeed I'm not sure that's what I want, but this seems like the first statically-typed FP language I like. I especially like how you can program the type level with constructs similar to the program level.