MarcelineVQ

--loop, I don't even use pffft
guess : (target : Nat) -> IO ()
guess target = do
  printLn "Rate die Zahl"
  line <- getLine
  Just g <- pure (stringToNat line) | Nothing => (printLn "Invalid String" *> guess target)
  let pffft = stringToNat line
  let g = case stringToNat line of
            Just p => p
            Nothing => 0

MarcelineVQ

effect :: (IsStream t, Monad m, Monad (t m)) => m (t m a) -> t m a
effect = join . S.yieldM

MarcelineVQ

data Foo = Bar | Baz

-- In haskell one can ensure coverage of the domain of a function (all cases of a datatype) by having ghc
-- tell you when a case is mising.
-- Can I ensure coverage of the codomain? (all outputs)

parse :: String -> Foo
parse "aba" = Bar
parse "za" = Baz -- how do I make it an error to omit this line? How can I make not covering Bar AND Baz a compiler error?

MarcelineVQ

<jusss> MarcelineVQ: but that's I do const a :: b -> a
<dmwit> What is the `a` in `const a`? It doesn't exist.
* EduardoBautista has quit (Ping timeout: 252 seconds)
* carif ([email protected]) has joined
* smasta has quit (Ping timeout: 268 seconds)
<MarcelineVQ> It means that Int and 3 live in different namespaces, Int is a type and 3 is a value. 3 doesn't belong to the right of :: and Int doesn't belong to the left.
* m-renaud (sid333785@gateway/web/irccloud.com/x-yvslmyywugovcxfp) has joined
* fnurglewitz (uid263868@gateway/web/irccloud.com/x-xhmjgnhcvxzyxenm) has joined
<fr33domlover> dmwit, in this case each thread has a TMVar (I'm using async package) and I just need to wait for them all to finish
* jusss` ([email protected]) has joined

MarcelineVQ

<mietek> moobar: https://twitter.com/valeriadepaiva/status/1119238128668012544
<mietek> > I definitely do NOT like idempotent monads or comonads. c'mon "possibly possible" is much weaker than "possible". sure, they're equiprovable, but not equivalent! see discussion in sec 8 of On an Intuitionistic Modal Logic, Bierman dePaiva
<mietek> dolio: ^^
<mietek> tomjack: ^^
<mietek> https://twitter.com/valeriadepaiva/status/1119254122719350784
<mietek> > Let me say it again: why I don't like idempotent (co-)monads. the point of doing it categorically, instead of using traditional oset models, is to have equiprovable, but not isomorphic types/propositions, if desired, correct?
<mietek> i’m a bit confused
* joomy has quit (Quit: My MacBook has gone to sleep. ZZZzzz…)
* joomy (~joomy@nat-oitwireless-outside-vapornet3-140-180-248-48.princeton.edu) has joined
* joomy has quit (Client Quit)

MarcelineVQ

data HList (ls :: [*]) where
  Nil :: HList '[]
  Cons :: x -> HList xs -> HList (x ': xs)

MarcelineVQ

syntax "(" [a] ",)" = \x => MkPair a x -- \x -> (a,x)
syntax "(," [a] ")" = \x => MkPair x a -- \x -> (x,a)

foo2 : Maybe Int -> Maybe (Int, Int)
foo2 n = (,3) <$> n

foo3 : Int -> (Int, Int)
foo3 n = ((,3)) n -- needs extra parens

MarcelineVQ

resolver: whatever

extra-deps:
- packagename-0.1.2

MarcelineVQ

formatNat : Nat -> String 
formatNat n with (isLTE 10 n)
  formatNat n | (Yes prf) = "." ++ show (n - 10)
  formatNat n | (No contra) = show n

MarcelineVQ

formatNat' : Nat -> String 
formatNat' n = case isLTE 10 n of
                 (Yes prf) => "." ++ show (n - 10)
                 (No contra) => show n