1ML – unifying ML into one language

Re:1ML – unifying ML into one language by octatoan on Thursday April 23, 2015 @03:02AM (#9425318)

If I remember correctly, isn't this one of the problems Idris and Agda are good at solving?

[ Parent | on HN ]

Re:1ML – unifying ML into one language by andolanra on Thursday April 23, 2015 @03:56AM (#9425433)

We could in fact write mkMap in Idris with very little change, and give it a proper type:

    -- This might not be the best/cleanest way of writing it, as my
    -- Idris is a little rusty, but this will work:
    mkMap : (size: Int) -> (if size > threshold then HashMap else TreeMap)
    mkMap size with (size > threshold)
      | True  = newHashMap
      | False = newTreeMap

So yes, although again, other tradeoffs are made to allow this kind of radical expressiveness.

[ Parent | on HN ]