xkcdAbout 20 Pounds
Recent searches
Search options
#haskell
7 posts6 participants0 posts today
#haskell question
An exercise wants me to write a function(s) such that it is interactive in ghci eg
> inc, status <- myfunction
>
> inc
> inc
> status
2
so I'm thinking about what inc and status are
* state must be held in myfunction - there's nowhere else for it to go
* inc updates the state
* status reads it
* so my function acts like a State Monad, or is an IO Monad a better fit?
* inc and status are related to myfunction by means of instance declaration ? Not sure.
Typed Lisp, a primer. ~ Musa Al-hassy (2019). https://alhassy.com/TypedLisp.html #CommonLisp #Haskell
alhassy.comTyped Lisp, A Primer
Typed Lisp 入門
➤ 探索 Lisp 的類型系統及其與 Haskell 的比較
✤ https://alhassy.com/TypedLisp.html
本文探討了 Lisp 的類型系統，並將其與 Haskell 進行比較。作者指出，雖然 Lisp 經常被認為是動態類型語言，但它實際上具有精細的類型層次結構，並且可以通過宏來實現靜態類型檢查。文章詳細介紹了 Lisp 的各種類型，例如數字、字符、符號、序列、函數和宏，並討論瞭如何使用 `deftype` 創建新的類型以及如何定義類似 Haskell 的代數數據類型。作者還強調了 Lisp 的靈活性和可擴展性，並認為它可以滿足對類型系統的各種需求。
+ "我一直覺得 Lisp 缺乏類型系統，這篇文章讓我重新認識了它。原來 Lisp 也可以有這麼豐富的類型表達能力！"
+ "作為一個 Haskell 愛好者，我對 Lisp 的靈活性感到好奇。文章很好地解釋了 Lisp 如何在保持動態特性的同時，也能夠利用類型來提高程式碼的可靠性。"
#Lisp #類型系統 #Haskell #編程語言
alhassy.comTyped Lisp, A Primer
The minimal megaparsec tutorial. ~ Clément Hurlin. https://www.tweag.io/blog/2025-04-24-minimal-megaparsec-tutorial/ #Haskell #FunctionalProgramming
www.tweag.ioThe minimal megaparsec tutorialThe shortest megaparsec tutorial there is to write your first DSL parser
How to control #superintelligence ?
IIUC, the approach here is to use provable languages like #Haskell to ensure the model does only the things you want and provably cannot do Bad Things.
How to deal with the required insanely large logic proofs? OFC, use #AI for that!
I'm missing something. What exact program do you want the machine to prove? Programs that the LLM writes? Or the LLM itself? Surely the latter is computationally intractable...?
arXiv.orgA Survey on Deep Learning for Theorem ProvingTheorem proving is a fundamental aspect of mathematics, spanning from informal reasoning in natural language to rigorous derivations in formal systems. In recent years, the advancement of deep learning, especially the emergence of large language models, has sparked a notable surge of research exploring these techniques to enhance the process of theorem proving. This paper presents a comprehensive survey of deep learning for theorem proving by offering (i) a thorough review of existing approaches across various tasks such as autoformalization, premise selection, proofstep generation, and proof search; (ii) an extensive summary of curated datasets and strategies for synthetic data generation; (iii) a detailed analysis of evaluation metrics and the performance of state-of-the-art methods; and (iv) a critical discussion on the persistent challenges and the promising avenues for future exploration. Our survey aims to serve as a foundational reference for deep learning approaches in theorem proving, inspiring and catalyzing further research endeavors in this rapidly growing field. A curated list of papers is available at https://github.com/zhaoyu-li/DL4TP.
Replied in thread
@easwatch #SevereWeather #OKwx #EAS #WEA for #Haskell, #OK; #Le Flore, #OK; #Sequoyah, #OK: National Weather Service: #TORNADO WARNING in this area until 1:45 PM CDT. Take shelter now in a basement or an interior room on the lowest floor of a sturdy building. If you are outdoors, in a mobile home, or in a vehicle, move to the closest substantial shelter and protect yourself from flying debris. Check media. Source: NWS Tulsa OK ** DO NOT RELY ON THIS FEED FOR LIFE SAFETY, SEEK OUT OFFICIAL SOURCES ***
Replied in thread
@easwatch #SevereWeather #OKwx #EAS #WEA for #Haskell, #OK; #Sequoyah, #OK: National Weather Service: #TORNADO WARNING in this area until 1:30 PM CDT. Take shelter now in a basement or an interior room on the lowest floor of a sturdy building. If you are outdoors, in a mobile home, or in a vehicle, move to the closest substantial shelter and protect yourself from flying debris. Check media. Source: NWS Tulsa OK ** DO NOT RELY ON THIS FEED FOR LIFE SAFETY, SEEK OUT OFFICIAL SOURCES ***
Replied in thread
@easwatch #SevereWeather #OKwx #EAS #WEA for #Haskell, #OK: National Weather Service: #TORNADO WARNING in this area until 12:45 PM CDT. Take shelter now in a basement or an interior room on the lowest floor of a sturdy building. If you are outdoors, in a mobile home, or in a vehicle, move to the closest substantial shelter and protect yourself from flying debris. Check media. Source: NWS Tulsa OK ** DO NOT RELY ON THIS FEED FOR LIFE SAFETY, SEEK OUT OFFICIAL SOURCES ***
Replied in thread
@easwatch #SevereWeather #OKwx #EAS #WEA for #Haskell, #OK: National Weather Service: #TORNADO WARNING in this area until 12:15 PM CDT. Take shelter now in a basement or an interior room on the lowest floor of a sturdy building. If you are outdoors, in a mobile home, or in a vehicle, move to the closest substantial shelter and protect yourself from flying debris. Check media. Source: NWS Tulsa OK ** DO NOT RELY ON THIS FEED FOR LIFE SAFETY, SEEK OUT OFFICIAL SOURCES ***
Replied in thread
my beginner brains wants to see
let b = f a
in Logger (something) b
because f is applied to a to get b
---
also the la++lb is confusing me because la is supplied as an argument but I can't see where lb comes from? there is no lb = ...
Replied to Ramin Honary
actually an hour later and I'm still not sure, so I went back to an earlier example in the #haskell course which I also don't understand
--
(#>) :: Logger a -> (a -> Logger b) -> Logger b
Logger la a #> f = let Logger lb b = f a -- feed value to next step
in Logger (la++lb) b -- bundle result with all messages
--
here again I'm seeing `let` but in an unfamiliar way
let "expression = epression" instead of let "variable = expression" .. I don't get it
new #haskell puzzle!
I'm trying to read and understand this code:
---
instance Monad Logger where
return x = Logger [] x
Logger la a >>= f = Logger (la++lb) b
where Logger lb b = f a
---
I'm familiar with simple `where` eg x = y where y = z + 1
but in this example the `y` in `where y =` doesn't actually appear in the preceding code.
hmmm...
---
does it patten match (la ++ lb) to lb in the where block? this doesn't make sense unless the two `lb` are not the same.
Not going to be able to do a stream tonight. I lost my voice! Should be back next week. #haskell
Replied in thread
@buherator no studies I know, but from personal experience using github copilot via vscod(ium) integration for #rustlang coding and having a functional programming background in #haskell, (data) types come first.. So my workflow is kind of
Either start with module header (rustdoc) natural language description and let the LLM help deriving the concrete datatypes, and/or:
Start with rust datatypes, let the llm derive rustdoc, fix it, let the llm refactor the datatypes.
Property-based testing in Haskell with QuickCheck
falsify A few days ago, Edsko de Vries of Well-Typed published an in-depth article on property-based software testing, with a focus on the concept of “shrinking.”
In brief, property-based testing is sort-of like fuzz testing but for algorithms and protocols. Like fuzz testing, random test cases are procedurally generated, but unlike fuzz testing, the test cases are carefully designed to verify whether a software implementation of an algorithm satisfies a specific property of that algorithm, such as:
- “this function always fails if the index is larger than the array”
- “this function always returns a result in
n*log(n)number of iterations for input dataset of sizen“ “the sequence of log messages is guaranteed to obey this rules of this particular finite-state automata: (connect | fail) -> (send X | fail) -> (receive Y | receive Z | fail) -> success .”
Shrinking is the process of simplifying a failed test case. If you have found some input that makes your function return a value when it should have thrown an exception, or produce a result that does not satisfy some predicate, then that input is a “counterexample” to your assertion about the properties of that function. And you may want to be able to “shrink” that counterexample input to see if you can cause the function to behave incorrectly again but with a simpler input. The “QuickCheck“ library provides a variety of useful tools to let you define property tests with shrinking.
Defining unit tests with such incredible rigor takes quite a lot of time and effort, so you would probably do not want to use property-based testing for your ordinary, every-day software engineering. If you are, for example, being scrutinized by the US Department of Government of Efficiency, you would likely be fired if you were to take so much time to write such high-quality software with such a strong guarantee of correctness.
But if you are, for example, designing a communication protocol that will be used in critical infrastructure for the next 10 or 20 years and you want to make sure the reference implementation of your protocol is without contradictions, or if you are implementing an algorithm where the mathematical properties of the algorithm fall within some proven parameters (e.g. computational complexity), property-based testing can give you a much higher degree of confidence in the correctness of your algorithm or protocol specification.
www.well-typed.comfalsify: Hypothesis-inspired shrinking for Haskell
New Book Launch! 
Unwrapping Monads & Friends by Kyle Simpson
https://leanpub.com/blog/new-book-launch-unwrapping-monads-friends-by-kyle-simpson
"Propositions as traits, proofs as impls"
I come to the point in #rustlang where I start feel comfortable with the #rustlang type system to do some serious type level programming... Noticable Effekt: where clauses blow up to a multiple of lines then the actual impl on value level, until it starts to hurt to factor out a new trait/impl pair.. This now feels (almost) as having back much of the missed stuff from #haskell land which could at least be compensated.