Innf107

Programming is about information not data, or: you might not need dependent types

When I took "Fundamentals of Computer Science" in college, my professor was very adamant about the distinction between data and information and about how data doesn't have any inherent meaning. At the time, it seemed a bit silly to me how much emphasis he put on such a seemingly insignificant difference.

In retrospect, I think he was exactly right about this and I wish more programmers took it to heart.

Data is something you can store in a computer, such as, let's say, the byte 0b01000001.

Innf107

#!/usr/bin/env polaris

module List = import("../polaris/lib/list.pls")

let filterMap : forall a b. (a -> < Nothing, Just(b) > , List(a)) -> List(b)
let filterMap(f, list) = match list {
    [] -> []
    (x :: xs) -> match f(x) {
        Nothing -> filterMap(f, xs)
        Just(y) -> y :: filterMap(f, xs)

Innf107

{-# LANGUAGE GHC2021, FunctionalDependencies, AllowAmbiguousTypes, OverloadedRecordDot, BlockArguments #-}
module Lib where

-- Code accompanying https://prophetlabs.de/posts/insttypes.html

import qualified Data.Map as Map

import Unsafe.Coerce

import Data.Proxy

Innf107

{-# LANGUAGE RankNTypes, PatternSynonyms, GADTs, ViewPatterns, LambdaCase, ScopedTypeVariables #-}
module Main where
    
import Data.Map as Map
import Control.Monad (ap, liftM)
import Data.IORef

data ComeFromOp a where
    Line :: Int -> ComeFromOp ()
    LiftIO :: IO () -> ComeFromOp ()