type-level stuff

cursedHaskell.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Main where

import System.IO
import Control.Monad

-- Booleans

data False

data True where
  I :: True

type family Not bool where
  Not False = True
  Not True = False

type family (&&) bool1 bool2 where
  True && True = True
  _ && _ = False

type family (||) bool1 bool2 where
  False || False = False
  _ || _ = True

type family (⇒) bool1 bool2 where
  True ⇒ False = False
  _ ⇒ _ = True

data Then
data Else

type family If cond then' branchTrue else' branchFalse where
  If True Then branch Else _ = branch
  If False Then _ Else branch = branch

-- Functions

type family ($) func arg where
  func $ arg = func arg

type family (|>) arg func where
  arg |> func = func arg

-- Pairs

type family First pair where
  First (left, _) = left

type family Second p where
  Second (_, right) = right

-- Nats

data O
data S n

type N1 = S O
type N2 = S N1
type N3 = S N2
type N4 = S N3
type N5 = S N4
type N6 = S N5
type N7 = S N6
type N8 = S N7
type N9 = S N8
type N10 = S N9

type family Succ n where
  Succ n = S n

type family Pred n where
  Pred O = O
  Pred (S n) = n

type family (==) n m where
  O == O = True
  S n == S m = n == m
  O == S _ = False
  S _ == O = False

type family (>) n m where
  O > _ = False
  _ > O = True
  S n > S m = n > m

type family (>=) n m where
  n >= m = n == m || n > m

type family (<) n m where
  O < _ = True
  _ < O = False
  S n < S m = n < m

type family (<=) n m where
  n <= m = n == m || n < m

type family (+) n m where
  n + O = n
  O + m = m
  n + S m = S n + m

type family (-) n m where
  n - O = n
  O - m = O
  S n - S m = n - m

type family (×) n m where
  n × O = O
  n × S m = n + (n × m)

-- assumption: m != 0
type family DivmodAuxUnsafe q n m where
  DivmodAuxUnsafe q n m =
    If (n < m)
    Then (q, n)
    Else (DivmodAuxUnsafe (S q) (n - m) m)

type family Divmod n m where
  Divmod n O = (O, O)
  Divmod n m = DivmodAuxUnsafe O n m

type family (/) n m where
  n / m = First (Divmod n m)

type family (%) n m where
  n % m = Second (Divmod n m)

type family Double n where
  Double n = n + n
  
type family Square n where
  Square n = n × n

type family SqrtAux n p q r where
  SqrtAux O p _ _ = p
  SqrtAux (S n) p q O = SqrtAux n (S p) (S (S q)) (S (S q))
  SqrtAux (S n) p q (S r) = SqrtAux n p q r

type family Sqrt n where
  Sqrt n = SqrtAux n O O O

type family Fact n where
  Fact O = S O
  Fact (S n) = S n × Fact n

type family Fib n where
  Fib O = O
  Fib (S O) = S O
  Fib (S (S n)) = Fib (S n) + Fib n

type family IsEven n where
  IsEven O = True
  IsEven (S O) = False
  IsEven (S (S n)) = IsEven n

type family IsOdd n where
  IsOdd n = Not (IsEven n)

-- List

data Nil
data Cons x xs

type family Repeat n value where
  Repeat O _ = Nil
  Repeat (S n) value = Cons value (Repeat n value)

type family Length list where
  Length Nil = O
  Length (Cons _ xs) = S O + Length xs

type family Map func list where
  Map _ Nil = Nil
  Map func (Cons first rest) = Cons (func first) (Map func rest)

type family RevConcat list1 list2 where
  RevConcat list1 Nil = list1
  RevConcat list1 (Cons first rest) = RevConcat (Cons first list1) rest

type family Reverse list where
  Reverse list = RevConcat Nil list

type family (++) list1 list2 where
  list1 ++ list2 = RevConcat list1 (Reverse list2)

type family (//) list index where
  Nil // n = (Nil, Nil)
  l // O = (Nil, l)
  Cons x xs // S n = (Cons x (First (xs // n)), Second (xs // n))

type family FoldLeft func acc list where
  FoldLeft _ acc Nil = acc
  FoldLeft func acc (Cons x xs) = FoldLeft func (func acc x) xs

testSlice ::
  Cons N3 (Cons N5 (Cons N2 Nil)) // N1 ≡ (Cons N3 Nil, Cons N5 (Cons N2 Nil))
testSlice = Eq

-- Propositional equality

data (≡) x y where
  Eq :: x ≡ x

onePlusOneEqTwo :: S O + S O ≡ S (S O)
onePlusOneEqTwo = Eq

-- Properties

plusIdRight :: n + O ≡ n
plusIdRight = Eq

plusIdLeft :: O + n ≡ n
plusIdLeft = Eq

main :: IO ()
main = return ()