4 ms·
If I remember correctly, isn't this one of the problems Idris and Agda are good at solving?
by octatoan 12y ago
If I remember correctly, isn't this one of the problems Idris and Agda are good at solving?
- andolanra 12y agoWe 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.