[Haskell-cafe] Re: practicality of typeful programming

[Pasqualino 'Titto' Assini]

Hi Daniil,

I had a look at the paper and associated code that Oleg refers to there is no 
special parsing taking place:

From Vector/read-examples.hs:

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:

<quote>
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)
<interactive>:1:0:
    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)
</quote>


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))
  return $
    (SigE
      (AppE (VarE $ mkName "fromList")
          (SigE es (AppT ListT et)))
      vt
    )

Crazy haskellers.

Is it just me that some time thinks with nostalgia to Apple II Basic?

Best,

       titto







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.