[Haskell-cafe] Re: practicality of typeful programming

[Daniil Elovkov]

2007/6/28, Pasqualino 'Titto' Assini <tittoassini at gmail.com>:
> On Wednesday 27 June 2007 23:28:44 oleg at pobox.com wrote:
> > In his system, the type of the matrix includes includes the matrix
> > size and dimensions, so invalid operations like improper matrix
> > multiplication can be rejected statically. And yet, his library
> > permits matrices read from files.
>
> Read from files but still at compile time, correct?

(titto, sorry for dupliate)

No, what is meant, I believe, is reading from a file at run-time and
parsing this way

(u :: UnTyped) <- readFromFile
case parse u of
    Nothing -> -- failed to parse, because those data wouldn't
satisfy constraints
    Just (t::Typed) ->
       -- if we're here, we have the typed t, and there are garantees
that it is well formed
       -- in terms of our invariants

parse :: UnTyped -> Maybe Typed

so deciding whether we have correct data is made at run-time, by
calling parse and examining its return value.