[Haskell-cafe] Re: practicality of typeful programming
Pasqualino 'Titto' Assini
tittoassini at gmail.com
Thu Jun 28 13:44:00 EDT 2007
I had a look at the paper and associated code that Oleg refers to there is no
special parsing taking place:
v3 = do
let m1 = $(dAM [[1,2],[3,4]])
s <- readFile "Vector/example-data.txt"
listMatRow (read s) (\(m2::AVector Double a) ->
print $ m2 *> trans m1
It does not make any difference if the list that is used to populate the
matrix is specified in the code or read from a file.
In both cases, if the list lenght is incorrect, an error is generated at
run-time (I think, I cannot run the actual code).
The TH trickery, that Oleg refers to, is there to solve a different problem:
Note that in each example we print the matrix _inside_ the function
argument to the list* functions. We cannot, for instance, just return
it, because this causes a universally quantified type to escape:
> listVec_ [1,2,3] (\v -> v)
Inferred type is less polymorphic than expected
Quantified type variable `n' escapes
In the second argument of `listVec', namely `(\ v -> v)'
In the definition of `it': it = listVec [1, 2, 3] (\ v -> v)
This is why it is not possible to have a function which takes a list
and returns a vector of unknown type. The 'fromList' member of the
Vector class is only used when we want to turn a list into a vector
whose type is known in advance. (see v4 below)
So, in order to play around with matrices of unknown type in GHCi what they do
(if I read the code correctly) is to convert the matrix to TH, specifying the
exact type, and compiling/splicing it back:
liftVec :: (GetType e, Lift e, GetType a, Dom a, Vector v e, GetType (v a))
=> v a -> ExpQ
liftVec (v::v a) = do
es <- lift (elems v)
let at = getType (__::a)
let et = getType (eltType v)
let vt = getType (__::(v a))
(AppE (VarE $ mkName "fromList")
(SigE es (AppT ListT et)))
Is it just me that some time thinks with nostalgia to Apple II Basic?
On Thursday 28 June 2007 15:38:17 Daniil Elovkov wrote:
> 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.
More information about the Haskell-Cafe