nkaretnikov

data Nat n where
  NZero :: Nat Zero
  NSucc :: forall n. Nat n -> Nat (Succ n)

intToNat :: Int -> forall n. Nat n
intToNat 0 = NZero
intToNat n = NSucc $ intToNat $ pred n

{-
    Couldn't match type ‘n’ with ‘Succ n0’

nkaretnikov

{-# LANGUAGE MagicHash #-}
{-# LANGUAGE UnboxedTuples #-}

module NotMain where

import GHC.Base

main :: IO ()
main =
  let (# w, i #) = subWordC# 1## 3##

nkaretnikov

.data
hello:
  .asciz "hello world %d\n"

.text
.globl main
main:
  subq $8, %rsp

  movb $0, %al

nkaretnikov

{-# LANGUAGE MagicHash #-}
{-# LANGUAGE UnboxedTuples #-}

module Main where

import Control.Monad
import GHC.Base
import GHC.Prim

main :: IO ()

nkaretnikov

GHCi, version 7.10.1: http://www.haskell.org/ghc/  :? for help
Prelude> let f x y = x + y
Prelude> f 2 _w
{-
<interactive>:5:5:
    Found hole ‘_w’ with type: a
    Where: ‘a’ is a rigid type variable bound by
               the inferred type of it :: a at <interactive>:5:1
    Relevant bindings include it :: a (bound at <interactive>:5:1)
    In the second argument of ‘f’, namely ‘_w’

nkaretnikov

-- f is a loop

main = do
  f foo
  bar
  
--
  
baz = do
  foo   -- called every time

nkaretnikov

\begin{eqnarray*}
\phantom{} & 2x(8 - x) = 0 & \phantom{} \\
2x = 0 & \text{или} & 8 - x = 0 \\
x = 0 & \text{или} & x = 8
\end{eqnarray*}

nkaretnikov

-- For haskell202

import Data.List (intercalate)

main :: IO ()
main = loop [] []
  where
    split = intercalate ", " . filter (not . null)
    loop animal attribute = do
      animal'    <- getLine

nkaretnikov

Theorem fact_3 :
  fact_in_coq / update empty_state X 3
              || (update
                    (update
                       (update
                          (update
                             (update
                                (update
                                   (update
                                      (update

nkaretnikov

Theorem optimize_plus_mult_l_sound: forall a,
  aeval (optimize_plus_mult_l a) = aeval a.
Proof.
  intros a. induction a.
    Case "ANum". reflexivity.
    Case "APlus". destruct a1.
      SCase "a1 = ANum".
        simpl. rewrite IHa2. reflexivity.
      SCase "a1 = APlus".
        simpl. destruct a1_1;