Haskell allow to use Functional dependencies. Using FD one can do Prolog-like things with types and classes. In compile time. Further: http://www.cse.chalmers.se/~hallgren/Papers/hallgren.pdf

fun-with-functional-dependencies.hs

{-# LANGUAGE FlexibleInstances, FunctionalDependencies, UndecidableInstances #-}
-- Esoteric programming with Haskell:
-- http://www.cse.chalmers.se/~hallgren/Papers/hallgren.pdf
-- https://repl.it/repls/AquaGainsboroSquares

module Fun where

data True
data False

data Zero
data Succ n

class Eval n where eval :: n -> Int
instance Eval Zero where eval _ = 0
instance Eval n => Eval (Succ n) where eval n = 1 + eval (predcs n) 

-- class Even n where isEven :: n
-- class Odd n where isOdd :: n

-- instance Even Zero
-- instance Odd n => Even (Succ n)
-- instance Even n => Odd (Succ n)

{-
 - in ghci:
 - :t isEven :: Three
 - :t isOdd :: Three
 -}

class Even n b | n -> b where isEven :: n -> b
class Odd n b | n -> b where isOdd :: n -> b

instance Even Zero True
instance Odd n b => Even (Succ n) b
instance Odd Zero False
instance Even n b => Odd (Succ n) b

{-
 - in ghci:
 - :t isEven (u :: Three)
 - :t isOdd (u :: Three)
 -}

class Add a b c | a b -> c where add :: a -> b -> c
instance Add Zero b b
instance Add a b c => Add (Succ a) b (Succ c)

{-
 - in ghci:
 - :t add (u :: Three) (u :: Three)
 -}

class Mul a b c | a b -> c where mul :: a -> b -> c
instance Mul Zero b Zero
instance (Mul a b c, Add b c d) => Mul (Succ a) b d

{-
 - in ghci:
 - :t mul (u :: Three) (u :: Three)
 -}

u = undefined

type One = Succ Zero
type Two = Succ (Succ Zero)
type Three = Succ (Succ (Succ Zero))
type Six = (Succ (Succ (Succ Three)))
type Twelve = Succ (Succ (Succ (Succ (Succ (Succ Six)))))
type Thirteen = Succ Twelve

class Pow a b c | a b -> c where pow :: a -> b -> c

instance Pow a Zero One
instance (Pow a b c, Mul a c d) => Pow a (Succ b) d

{-
 - in ghci:
 - :t pow (u :: Three) (u :: Three)
 -}

class Pred a b | a -> b where predcs :: a -> b
instance Pred (Succ n) n

class Power n where power :: Int -> n -> Int
instance Power Zero where power _ _ = 1
instance Power n => Power (Succ n) where
    power x n = x * power x (predcs n)

{-
 - in ghci:
 - power 2 (mul (u::Three) (u::Three)) 
 -}

data T = T
data F = F

data Nil = Nil
data Cons x xs = Cons

class DownFrom n xs | n -> xs where downfrom :: n -> xs
instance DownFrom Zero Nil
instance DownFrom n xs => DownFrom (Succ n) (Cons n xs)

class Lte a b c | a b -> c  where lte :: a -> b -> c
instance Lte Zero b T
instance Lte (Succ n) Zero F
instance Lte a b c => Lte (Succ a) (Succ b) c

class Insert x xs ys | x xs -> ys where insert :: x -> xs -> ys
instance Insert x Nil (Cons x Nil)
instance (Lte x y b, InsertCons b x y ys r) => Insert x (Cons y ys) r
class InsertCons b x1 x2 xs ys | b x1 x2 xs -> ys
instance InsertCons T x1 x2 xs (Cons x1 (Cons x2 xs))
instance Insert x1 xs ys => InsertCons F x1 x2 xs (Cons x2 ys)
class Sort xs ys | xs -> ys where sort :: xs -> ys
instance Sort Nil Nil
instance (Sort xs ys, Insert x ys zs) => Sort (Cons x xs) zs

l1 = downfrom (u::Three)
{-
 - in ghci:
 - :t l1
 - :t sort l1
 - :t sort (u::Cons Six (Cons Thirteen (Cons Three (Cons One (Cons Six Nil))))) 
 -}