[Haskell] (Succ Haskell') `and` $ dependent types
Hello, As the authors point out [1], coal-face time needs to be expended before real world adoption of Dependently-Typed functional programming. But let's get the ball rolling. They say that haskell programmers are normally averse to dependent types. Is this true? It seems to me that one of the appeals of Haskell is the ability to program in a "prove perfect, write once" (elegant) style. Is not dependent typing a good move towards this goal?. It addresses a problem [2] with which we, in our everyday common inter-hominem usage, can deal -- with which (ideal) Haskell should deal. While the major Haskell implementations would require a substantial overhaul, the change at the syntactic level appears to be minimal. There also needs to be advance with respect to programmer development (automatic edit-time inference of (some) types). What are peoples' thoughts on adding dependent types to haskell as a non-incremental evolutionary step? Does the haskell community want to stick with conservative additions to Haskell and a static base, or does the haskell community want to stay in step with the best theoretical developments? Vivian [1] http://www.informatik.uni-bonn.de/~loeh/LambdaPi.html [2] http://thread.gmane.org/gmane.comp.lang.haskell.cafe/21314 ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] sweet bananas, lenses, and other miscellaneous brackets
Hi,
Just as we can define infix operators as syntactic sugar,
could we not also have a similar mechanism for programmable fancy
brackets?
There could be a keyword for the bracket declaration and a
function definition, in this way ana- and catamorphisms, Template Haskell-like
syntax, and set notation could become a regular feature of the language. I
am more interested in the general idea than the syntax of this specific
example:
\begin{code}
bracket (( _ )) :: a -> Ana a
bracket (| _ |) :: a -> Cata a
bracket [ _ | _ |] :: Char -> b
-> Splice -- or whatever
bracket {[ _ , .. ]} :: [a] -> SList a
((( _ ))) :: a -> Ana a
(( x )) = Ana x
((| _ |)) :: a -> Cata a
(| x |) = Cata x
([ _ | _ |]) :: Char -> b -> Splice
[ c | t |] = case c of
b
-> doC t
d
-> doD t -- or whatever
-- the idea of this bracket is to create a user-defined
list-type structure
-- {[ "the" , "lambda" , "calculus"
]}
-- would have the value
--(SCons "the" (SCons "lambda" (SCons
"calculus" SEmpty)))
({[ _ , .. ]} :: [a] -> SList a
{[ [] ]} = sempty
{[ x:xs ]} = scons x {[ xs ]}
\end{code}
Any thoughts?
Vivian
___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
[Haskell] manipulating untyped lambda-calculus in Haskell
Hi,
I am writing a NL parser in Haskell, relying on combinatorial
grammar for the syntactic derivation.
Each word has an associated syntax and semantics, the semantic
term is a lambda _expression_ loaded at run-time using hs-plugins.
I : np :
:: Sem m a
love : s\np : :: Sem m a
Predicates in english can have up to 5 arguments, and some of
these arguments are functions, so the type of Sem m a is an enumeration of the
types that we can build up from (STT m a) and (->).
I started by enumerating this by hand:
\begin{code}
data Monad m => Sem m a = ZSem (SST m
a) | USem (SST m a -> SST m a) |
BSem (SST m a -> SST m a -> SST m a) | TSem (SST m a
-> SST m a -> SST m a -> SST m a) | QSem (SST m a
-> SST m a -> SST m a -> SST m a -> SST m a) |
FSem (SST m a -> SST m a -> SST m a -> SST m a -> SST m a ->
SST) -- | U1Sem ((SST m a -> SST m
a) -> SST m a) | B1Sem ((SST m a -> SST m a) ->
SST m a -> SST m a) | T1Sem ((SST m a -> SST m a)
-> SST m a -> SST m a -> SST m a) \end{code}
then what I need is a function to apply these:
\begin{code}
applySem :: Monad m => Sem m a -> Sem m a -> Sem m
aapplySem (USem a) (ZSem b) = ZSem $ a bapplySem (BSem a) (ZSem b) =
USem $ a bapplySem (TSem a) (ZSem b) = BSem $ a bapplySem (QSem a) (ZSem
b) = TSem $ a bapplySem (U1Sem a) (USem b) = ZSem # a b applySem (B1Sem
a) (USem b) = USem $ a bapplySem (T1Sem a) (USem b) = BSem $ a bapplySem
(T2Sem a) (ZSem b) = B1Sem $ a bapplySem (B12Sem a) (USem b) = U1Sem $ a
bapplySem _
_ = error "application of Semantic
functions"\end{code}
My typing system ensures that only the correct functions will
be applied to each other (the typing system manipulates lambda terms with an
additional type (Stc Name (Sem m a)). A complete parse will reduce the
lambda terms to closed terms containing only App and Stc, no Var or Lam. I
can then use applySem to reduce the term to a single (Sem m a) type, which I can
then run.
What I have done thus far is enumerate by hand, but for full
coverage for 5 argument predicates I need to list 5^5 data constructors and
entries in the applySem function. For theoretically complete coverage I
would need to enumerate all possible types constructed from (STT m a) and
(->).
It seems that I must be missing something? Is there a
more elegant way of doing this?
One can make the observation that the applySem function
always applies a function of type (b -> a) to a function of type b to
yield a function of type a.
I suppose I could write a code generator (in
haskell) that enumerates all possible derivations of (STT m a) and (->)
but there would still be 5^5 data constructors.
Thanks,
Vivian McPhail
PS Is there something I can do with the Typeable class of
hs-plugins?
___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
[Haskell] Running haskell from within Haskell
Dear All, I have a parser which has entries for each word, such as: ate = s \ np / np : ^x y.did(eat y x); so each word has a type (s \ np / np) and a semantics (the lambda term ^x y.did(eat y x)). Currently I parse the semantics into lambda terms and use my own lambda-interpreter to do evaluation. "I ate a python programmer" would be evaluated as: did(eat I (a python programmer)) What I would like to be able to do is actually use haskell functions in the semantic slot for each word. This requires parsing a fragment of a file into haskell and then making it available as code within my program. Is this possible? for example: kicked = s \ np / np : \x y -> case x of (the bucket) = did(die y) _= did(kick y x); Thanks in advance. Vivian ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] Simple question about IO in hugs and ghc
Hi,
When I run my main function I get an error:
The prompt does not wait for user input and thus my parser
fails with an empty head.
Is there a switch to not echo to the console? Is this
the problem? It happens in both Hugs and GHC
main :: IO ()main = do
putStr "sentence?
" input <-
getLine case input
of "quit" ->
putStr "bye.\n"
_ -> do
let res = get_result $
proof $ do_proof $ getInput input
in if res ==
Nothing
then putStr ("->
Nothing\n")
else putStr ("-> " ++ (show $ unJust
res) ++ "\n")
main
Sample output:
START>
$ mmccg.exe
sentence?
Fail: Prelude.head: empty list
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
[Haskell] State Transformers and Control.Monad.ST.Lazy
Hi,
>From the very helpful posts of John Hughes and others concerning
"Monadic Loops", I've been advised to re-implement my neural net
simulator using lazy state threads to avoid crashes to which recursive
(and tail-recursive) monads lead.
I had been using monad transformers to lift IO operations:
data NeuralNet = NN { ... }
data NNO a = NNO (NeuralNet -> (a,NeuralNet))
data NNT m a = NNT (NeuralNet -> m (a,NeuralNet))
following the example of a state transformer in "Functional Programming
with Overloading and Higher-Order Polymorphism".
I am trying to reimplement with
data ST s a
from Control.Monad.ST.Lazy and "Lazy Functional State Threads"
however there is something I think I do not understand, that is the "s" in
the ST dataype. The compiler tells me it needs to be instantiated, but I am
presuming that a type such as
type NNST = ST NeuralNet a
is useless because there is no way (from this module) to access that
state using the "update" method of the MonadState class.
1. Am I correct in thinking that I need to use a monad transformer lifting
from the ST monad to incorporate my NeuralNet datatype
2. Can I merely instantiate ST as ST () a?
Thanks in advance.
Vivian McPhail
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
[Haskell] Monadic Loops
Hi, I've implemented a Neural Net simulator which needs to repeat a training loop many times. For this I used a while function: while test body = do (cond,res) <- body if (test cond) then do rs <- while test body return (res:rs) else return [res] However, when I run the program, the interpreter falls over after a few thousand iterations, running out of space. I think that this is because the Monadic implementation of the while loop actually nests functions of type (a -> M b) and there is a maximum ?stack size. Is there a better way to implement (possibly infinite) loops in Haskell? ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
[Haskell] Monadic Loops
Hi, I've implemented a Neural Net simulator which needs to repeat a training loop many times. For this I used a while function: while test body = do (cond,res) <- body if (test cond) then do rs <- while test body return (res:rs) else return [res] However, when I run the program, the interpreter falls over after a few thousand iterations, running out of space. I think that this is because the Monadic implementation of the while loop actually nests functions of type (a -> M b) and there is a maximum ?stack size. Is there a better way to implement (possibly infinite) loops in Haskell? ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
