AntC

0

votes
0

answer
6

views

Data types a la carte — over-engineered?

I'm working through Swiertstra's 2008 paper. I'm up to Section 3 eval addExample, just before 'Automating injections'. And boy! does it need automating. Is it just me, or is the whole thing over-engineered? Compare this in the paper addExample :: Expr (Val :+: Add) addExample = In (Inr (Add (In (Inl...
AntC
1

votes
2

answer
163

views

Anonymous records: what ways to type-level tag in Haskell?

I'm playing with lightweight anonymous record-alikes, more to explore the type theory for them than anything 'industrial strength'. I want the fields to be simply type-tagged. myRec = (EmpId 54321, EmpName 'Jo', EmpPhone '98-7654321') -- in which newtype EmpPhone a = EmpPhone a...
AntC
1

votes
0

answer
102

views

Pattern synonyms deriving read?

Pattern synonyms provide a shorthand way to express a value; also they can provide an abstract name to avoid a client module breaking into the data decl. Here's a not very useful one, as an example for discussion: data MyNum = MkNum Int pattern Zero :: MyNum pattern Zero = MkNum 0 What I can do to h...
AntC
1

votes
0

answer
189

views

Haskell Functional Dependencies Consistency Condition: is it needed? Is it used?

The FunDep Consistency Condition appears in all the literature dating back to Mark P Jones 2000 paper. And it's inherited from the database-theory origins of FunDeps. But Haskell's FunDeps are not very much like in databases: a FunDep -> means: in any instance for this class, I promise to give an al...
AntC
8

votes
2

answer
126

views

Strange tilde syntax

GHC accepts this code, but it ought to be illegal syntax(?) Any guesses as to what's going on? module Tilde where ~ x = x + 2 -- huh? ~ x +++ y = y * 3 -- this makes sense The (+++) equation makes sense: it's declaring an operator, using infix syntax, and using an irrefutable patt...
AntC
1

votes
1

answer
177

views

Removing text in a <sup> tag from a span while scraping the rest of the text

I'm trying to scrape text with beautiful soup and I need to get text from inside a span with a specific class but discard the superscript numbers inside the same span with a different class. I can very easily use get_text to pull the number and the contents from the span but I end up with the supers...
antc
2

votes
2

answer
270

views

Prover9 hints not being used

I'm running some Lattice proofs through Prover9/Mace4. I'm using a non-standard axiomatization of the lattice join operation, from which it is not immediately obvious that the join is commutative, associative and idempotent. (I can get Prover9 to prove that it is -- eventually.) I know that Prover9...
AntC
7

votes
2

answer
287

views

differences: GADT, data family, data family that is a GADT

What/why are the differences between those three? Is a GADT (and regular data types) just a shorthand for a data family? Specifically what's the difference between: data GADT a where MkGADT :: Int -> GADT Int data family FGADT a data instance FGADT a where -- note not FGADT Int MkFGADT...
AntC