Fix SimpleDataRealizedFunction

[sroberti]

I changed the definition of SimpleDataRealizedFunction slightly to be parameterized on the Type of the function it represents, rather than the function itself (though it still takes that function as an argument to the constructor). This should allow it to represent functions with any number of arguments, just in case that's required later.

The composition and application functions mostly just needed to have all arguments passed to the MkSimpleDataRealizedFunction constructors.

I've also added %default total to both files, which is something I recommend doing in general unless it starts causing problems in specific cases.

[ngeiswei]

Thanks @sroberti, it looks good! I like the use of Repl, something I haven't gotten used to yet. I also agree that's it's better to have SimpleDataRealizedFunction parameterized on the function type than the function itself (that's actually what I wanted to do but I was confused at the time).

Small detail, I think it's possible to have MkSimpleDataRealizedFunction take only the function as arguments as opposed to function + cost and quality, just like MkSimpleRealizedFunction. Do you think it is desirable (I wouldn't see why not, as it seems like a harmless simplification, but I'm not sure)? And if so could you add up another commit with that small simplification?

[sroberti]

It might be possible to remove the cost + quality arguments from the constructor, but that may not give us the proof we'd want here. MkSimpleDataRealizedFunction : (f : t) -> SimpleDataRealizedFunction t cost quality will typecheck just fine, but it would also have the ability to construct a SimpleDataRealizedFunction for any value of cost or quality instead of being constrained to the values that match the actual attributes of the function.

I've been working on a similar Type that might give the guarantees we'd want here; It's not final, but I'll try and include it in a bit once I've cleaned it up a bit.

[sroberti]

The test cases in that file aren't complete, but the Service type shows how composition laws can be encoded in a type definition rather than an external function. This line of thinking is a work in progress, though, since I'm still working out how best to handle the function application phase.

[ngeiswei]

I think it's a good direction you're heading to with Service. And I agree that we want to be as abstract as possible when formalizing composition laws for all arrangements, sequential, parallel, conditional, etc.

[ngeiswei]

BTW, @sroberti, it's generally better to work on forks of master rather than master itself. That is purely for logistic reasons, it makes it easier to work on multiple things in parallel. Say you're working on two things, 1) fixing a bug and 2) adding a new feature, then you can create 2 branches from your local master, called for instance fix-123 and add-xyz. Once you're done, you can create PRs with these branches. On top of being easier to organize your work it's also easier for others to fetch and test (it helps to give intelligible names to the branches as well).