cheery

module Linc where

import Data.STRef
import Control.Monad.ST
import Control.Monad ((>=>))

data Structure = Structure
    { term       :: Tm Int Int
    , link_count :: Int
    , opt_count  :: Int

Rotsor

-- a proof of monad laws for a strange monad defined in:
-- https://www.reddit.com/r/haskell/comments/cb1j40/is_there_a_valid_monad_instance_for_binary_trees/etcqsts/

data TREE (a : Set) : Set where
  Leaf : a → TREE a
  Tree : a → TREE a → TREE a → TREE a

distribute : ∀ {a} → (TREE a) -> (TREE a) -> (TREE a) -> TREE a
distribute l r (Leaf a) = Tree a l r
distribute l r (Tree a cl cr) = Tree a (distribute l r cl) (distribute l r cr)

madidier

-- I haven't been able to actually run the program (broken archlinux packages), but it typechecks

open import Data.String
open import Function
open import IO.Primitive

Either : Set → Set → Set₁
Either l r = {a : Set} → (l → a) → (r → a) → a 

Left  : { l r : Set } → l → Either l r

gelisam

At work, I just spent the last few weeks exploring and evaluating every format I could find, and my number one criteria was whether they supported sum types. I was especially interested in schema languages in which I could describe my types and then some standard specifies how to encode them using an on-the-wire format, usually JSON.

1. Swagger represents sum types like Scala does, using subtyping. So you have a parent type EitherIntString with two subtypes Left and Right represented as {"discriminator": "Left", value: 42} and {"discriminator": "Right", value": "foo"}. Unfortunately, unlike in Scala in which the parent type is abstract and cannot be instantiated, in Swagger it looks like the parent type is concrete, so when you specify that your input is an EitherIntString, you might receive {"discriminator": "EitherIntString"} instead of one of its two subtypes.
2. JSON-schema supports unions, which isn't quite the same thing as sum types because